Show simple item record

dc.contributor.authorAbío Roig, Ignasi
dc.contributor.authorNieuwenhuis, Robert Lukas Mario
dc.contributor.authorOliveras Llunell, Albert
dc.contributor.authorRodríguez Carbonell, Enric
dc.contributor.authorStuckey, Peter
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics
dc.identifier.citationAbío, I. [et al.]. To encode or to propagate? The best choice for each constraint in SAT. A: International Conference on Principles and Practice of Constraint Programming. "Principles and Practice of Constraint Programing - CP 2013 19th International Conference, CP 2012, Uppsala, Sweden, September 16-20, 2013, Proceedings". Uppsala: Springer, 2013, p. 97-106.
dc.description.abstractSophisticated 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 approach, SMT). For example, given a cardinality constraint x 1 + … + x n  ≤ k, as soon as k variables become true, such a propagator can set the remaining variables to false, generating a so-called explanation clause of the form x1∧…∧xk→xi¯ . But certain “bottle-neck” constraints end up generating an exponential number of explanations, equivalent to a naive SAT encoding, much worse than using a compact encoding with auxiliary variables from the beginning. Therefore, Abío and Stuckey proposed starting off with a full SMT approach and partially encoding, on the fly, only certain “active” parts of constraints. Here we build upon their work. Equipping our solvers with some additional bookkeeping to monitor constraint activity has allowed us to shed light on the effectiveness of SMT: many constraints generate very few, or few different, explanations. We also give strong experimental evidence showing that it is typically unnecessary to consider partial encodings: it is competitive to encode the few really active constraints entirely. This makes the approach amenable to any kind of constraint, not just the ones for which partial encodings are known.
dc.format.extent10 p.
dc.subjectÀrees temàtiques de la UPC::Informàtica::Programació
dc.subject.lcshConstraint programming (Computer science)
dc.subject.otherActive constraints
dc.subject.otherAuxiliary variables
dc.subject.otherCardinality constraints
dc.subject.otherCompact encoding
dc.subject.otherExperimental evidence
dc.subject.otherExponential numbers
dc.subject.otherOn the flies
dc.subject.otherSat modulo theories
dc.titleTo encode or to propagate? The best choice for each constraint in SAT
dc.typeConference report
dc.subject.lemacProgramació per restriccions (Informàtica)
dc.contributor.groupUniversitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
dc.rights.accessOpen Access
dc.description.versionPostprint (author’s final draft)
local.citation.authorAbío, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Stuckey, P.
local.citation.contributorInternational Conference on Principles and Practice of Constraint Programming
local.citation.publicationNamePrinciples and Practice of Constraint Programing - CP 2013 19th International Conference, CP 2012, Uppsala, Sweden, September 16-20, 2013, Proceedings

Files in this item


This item appears in the following Collection(s)

Show simple item record

All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder