To Encode or to Propagate? The Best Choice for Each Constraint in SAT

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, ..