To encode or to propagate? The best choice for each constraint in SAT

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

12 Citations (Scopus)

Abstract

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 approach, SMT). For example, given a cardinality constraint x1 +...+ xn ≤ 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 → x ī. 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.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming - 19th International Conference, CP 2013, Proceedings
PublisherSpringer
Pages97-106
Number of pages10
ISBN (Print)9783642406263
DOIs
Publication statusPublished - 22 Oct 2013
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2013 - Uppsala, Sweden
Duration: 16 Sept 201320 Sept 2013
Conference number: 19th
http://cp2013.a4cp.org/

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8124 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2013
Abbreviated titleCP 2013
Country/TerritorySweden
CityUppsala
Period16/09/1320/09/13
Internet address

Cite this