Browsing by Author "Nieuwenhuis, Robert Lukas Mario"
Now showing items 1-11 of 11
-
A parametric approach for smaller and better encodings of cardinality constraints
(Springer, 2013)
Conference report
Open AccessAdequate 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
(Springer Verlag, 2011)
Conference report
Restricted access - publisher's policyPseudo-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
(Springer, 2009)
Conference report
Restricted access - publisher's policyWe 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
(2002-06-06)
External research report
Open AccessThe 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.)
(Universitat Politècnica de Catalunya, 2002-01-15)
Exam
Restricted access to the UPC academic community -
COMPILADORS I (Examen 1r quadrim.)
(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
(2016)
Article
Restricted access - publisher's policyConflict-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
(Springer Verlag, 2011)
Conference report
Restricted access - publisher's policyMotivated 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
(2007-01)
External research report
Open AccessEl 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
(Springer, 2014)
Conference report
Open AccessConflict-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
(Springer, 2013)
Conference report
Open AccessSophisticated 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 ...
