Translating Pseudo-Boolean Constraints into SAT

By Niklas Eén, Niklas Sörensson. Journal on Satisfiability, Boolean Modeling and Computation, 2006

721 citations recorded by the source corpus.

In this paper, we describe and evaluate three different techniques for translating pseudo-boolean constraints (linear constraints over boolean variables) into clauses that can be handled by a standard SAT-solver. We show that by applying a proper mix of translation techniques, a SAT-solver can perform on a par with the best existing native pseudo-boolean solvers. This is particularly valuable in those cases where the constraint problem of interest is naturally expressed as a SAT problem, except for a handful of constraints. Translating those constraints to get a pure clausal problem will take full advantage of the latest improvements in SAT research. A particularly interesting result of this work is the efficiency of sorting networks to express pseudo-boolean constraints. Although tangential to this presentation, the result gives a suggestion as to how synthesis tools may be modified to produce arithmetic circuits more suitable for SAT based reasoning.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/cf253eac1a2c9e610f745466d1ad00255bd8b7e5

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Networks and Communications

Citations in the corpus

Core-Boosted Linear Search for Incomplete MaxSAT (2019, methodology): “Depending on the specific encoding used, the number of clauses resulting from encoding PB into CNF depends either on the magnitudes of the weights of the soft clauses and the right-hand side [23] or on the number of unique sums that can be created from those weights [27].”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, methodology): “For pseudo-Boolean constraints available CNF encodings in the literature include BDDs [45], sorting networks [45] and the Warners’ encoding [125] .”
Efficient SAT-Based Encodings of Conditional Cardinality Constraints (2018, methodology): “One of the most effective encodings for cardinality constraints is based on sorting networks [8].”
Kodkod: A Relational Model Finder (2007, methodology): “The fourth step is performed using the standard translation from boolean logic to conjunctive normal form (see, for example, [29]).”
Conflict-driven answer set solving: From theory to practice (2012, methodology): “In contrast to translational approaches, as used by minisat+ [36], it offers dedicated data structures for the internal representation of and reasoning about linear inequalities [47].”
Solving MAXSAT by Decoupling Optimization and Satisfaction (2014, background): “Marques-Silva and Planes chose a more e cient BDD-based encoding, that adds only a linear number of variables and clauses (Marques-Silva and Planes, 2007; Eén and Sörensson, 2006).”