Enviaments recents

  • Employee scheduling with SAT-based pseudo-boolean constraint solving 

    Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rollón Rico, Emma (Institute of Electrical and Electronics Engineers (IEEE), 2021)
    Article
    Accés obert
    The aim of this paper is practical: to show that, for at least one important real-world problem, modern SAT-based technology can beat the extremely mature branch-and-cut solving methods implemented in well-known state-of-the-art ...
  • A heuristic approach to the design of optimal cross-docking boxes 

    Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Institute of Electrical and Electronics Engineers (IEEE), 2021-09-03)
    Article
    Accés obert
    Multinational companies frequently work with manufacturers that receive large orders for different products (or product varieties: size, shape, color, texture, material), to serve thousands of different final destinations ...
  • Incomplete SMT techniques for solving non-linear formulas over the integers 

    Borralleras Andreu, Cristina; Larraz Hurtado, Daniel; Rodríguez Carbonell, Enric; Oliveras Llunell, Albert; Rubio Gimeno, Alberto (2019-08-01)
    Article
    Accés obert
    We present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas ...
  • Short proofs of the Kneser-Lovász coloring principle 

    Aisenberg, James; Bonet Carbonell, M. Luisa; Buss, Sam; Craciun, Adrian; Istrate, Gabriel (2018-08)
    Article
    Accés obert
    We prove that propositional translations of the Kneser–Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs for all fixed values of k. We present a new counting-based combinatorial ...
  • Are crossing dependencies really scarce? 

    Ferrer Cancho, Ramon; Gómez Rodríguez, Carlos; Esteban Ángeles, Juan Luis (2018-03-01)
    Article
    Accés obert
    The syntactic structure of a sentence can be modelled as a tree, where vertices correspond to words and edges indicate syntactic dependencies. It has been claimed recurrently that the number of edge crossings in real ...
  • Subproblem ordering heuristics for AND/OR best-first search 

    Lam, William; Kask, Kalev; Larrosa Bondia, Francisco Javier; Dechter, Rina (2017-11-09)
    Article
    Accés obert
    Best-first search can be regarded as anytime scheme for producing lower bounds on the optimal solution, a characteristic that is mostly overlooked. We explore this topic in the context of AND/OR best-first search, guided ...
  • Residual-guided look-ahead in AND/OR search for graphical models 

    Lam, William; Kask, Kalev; Larrosa Bondia, Francisco Javier; Dechter, Rina (2017-10-01)
    Article
    Accés obert
    We introduce the concept of local bucket error for the mini-bucket heuristics and show how it can be used to improve the power of AND/OR search for combinatorial optimization tasks in graphical models (e.g. MAP/MPE or ...
  • Jutge.org: characteristics and experiences 

    Petit Silvestre, Jordi; Roura Ferret, Salvador; Carmona Vargas, Josep; Cortadella, Jordi; Duch Brown, Amalia; Giménez, Omer; Mani, Anaga; Mas Rovira, Jan; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto; San Pedro Martín, Javier de; Venkataramani, Divya (2018-07)
    Article
    Accés obert
    Jutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics and difficulty. Internally, Jutge.org uses a ...
  • A correction on Shiloach's algorithm for minimum linear arrangement of trees 

    Esteban Ángeles, Juan Luis; Ferrer Cancho, Ramon (2017-06-29)
    Article
    Accés obert
    More than 30 years ago, Shiloach published an algorithm to solve the minimum linear arrangement problem for undirected trees. Here we fix a small error in the original version of the algorithm and discuss its effect on ...
  • Improving IntSat by expressing disjunctions of bounds as linear constraints 

    Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario (2016)
    Article
    Accés restringit per política de l'editorial
    Conflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates ...
  • Quasipolynomial size frege proofs of Frankl's Theorem on the trace of sets 

    Aisenberg, James; Bonet Carbonell, M. Luisa; Buss, Sam (2016-06-01)
    Article
    Accés obert
    We extend results of Bonet, Buss and Pitassi on Bondy's Theorem and of Nozaki, Arai and Arai on Bollobas' Theorem by proving that Frankl's Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant ...
  • The scaling of the minimum sum of edge lengths in uniformly random trees 

    Esteban Ángeles, Juan Luis; Ferrer Cancho, Ramon; Gómez Rodríguez, Carlos (Institute of Physics (IOP), 2016-06-21)
    Article
    Accés obert
    The minimum linear arrangement problem on a network consists of finding the minimum sum of edge lengths that can be achieved when the vertices are arranged linearly. Although there are algorithms to solve this problem on ...

Mostra'n més