Now showing items 1-11 of 11

    • A parametric approach for smaller and better encodings of cardinality constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2013)
      Conference report
      Open Access
      Adequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular, cardinality constraints state that at most (at least, or exactly) k out of n propositional variables ...
    • BDDs for Pseudo-Boolean Constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer Verlag, 2011)
      Conference report
      Restricted access - publisher's policy
      Pseudo-Boolean constraints are omnipresent in practical applications, and therefore a significant effort has been devoted to the development of good SAT encoding techniques for these constraints. Several of these encodings ...
    • Cardinality networks and their applications 

      Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2009)
      Conference report
      Restricted access - publisher's policy
      We introduce Cardinality Networks, a new CNF encoding of cardinality constraints. It improves upon the previously existing encodings such as the sorting networks of [ES06] in that it requires much less clauses and auxiliary ...
    • Classes of term rewrite systems with polynomial confluence problems 

      Godoy Balil, Guillem; Nieuwenhuis, Robert Lukas Mario (2002-06-06)
      External research report
      Open Access
      The confluence property of ground (i.e., variable-free) term rewrite systems (GTRS) is well-known to be decidable. This was proved independently in [DTHL87,DHLT90] and in [Oya87] using tree automata techniques and ground ...
    • COMPILADORS I (Examen 1r quadrim.) 

      Nieuwenhuis, Robert Lukas Mario (Universitat Politècnica de Catalunya, 2002-01-15)
      Exam
      Restricted access to the UPC academic community
    • COMPILADORS I (Examen 1r quadrim.) 

      Nieuwenhuis, Robert Lukas Mario (Universitat Politècnica de Catalunya, 2002-01-15)
      Exam
      Restricted access to the UPC academic community
    • Improving IntSat by expressing disjunctions of bounds as linear constraints 

      Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario (2016)
      Article
      Restricted access - publisher's policy
      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 ...
    • Reducing chaos in SAT-like search: finding solutions close to a given one 

      Abío Roig, Ignasi; Deters, Morgan; Nieuwenhuis, Robert Lukas Mario; Stuckey, Peter (Springer Verlag, 2011)
      Conference report
      Restricted access - publisher's policy
      Motivated by our own industrial users, we attack the following challenge that is crucial in many practical planning, scheduling or timetabling applications. Assume that a solver has found a solution for a given hard ...
    • Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland 

      Gabriel Cerna, Pedro Víctor; Nieuwenhuis, Robert Lukas Mario (2007-01)
      External research report
      Open Access
      El problema de satisfación de fórmulas lógicas (SAT), es un problema NP-Hard. Una forma de resolverlo es por medio de procedimientos Davis-Putnam-Longemann-Loveland (DPLL), ahora presentamos una implementación de un ...
    • The IntSat method for integer linear programming 

      Nieuwenhuis, Robert Lukas Mario (Springer, 2014)
      Conference report
      Open Access
      Conflict-Driven Clause-Learning (CDCL) SAT solvers can automatically solve very large real-world problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraints, ...
    • To encode or to propagate? The best choice for each constraint in SAT 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter (Springer, 2013)
      Conference report
      Open Access
      Sophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo Theories ...