Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems

DOI10.1613/JAIR.3809MaRDI QIDQ4913754zbMATH OpenOpenAlexWikidataFDO

Authors Amit Metodi, Michael Codish, Peter J. Stuckey

Publication date 9 April 2013

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.0568

zbMATH Keywords

SAT encodingcombinatorial problemsBoolean equi-propagation

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Combinatorial optimization (90C27)

Abstract: We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one time enables us to apply stronger, and even complete, reasoning to detect equivalent literals in that fragment. Once detected, equivalences apply to simplify the entire constraint model and facilitate further reasoning on other fragments. Equi-propagation in combination with partial evaluation and constraint simplification provide the foundation for a powerful approach to SAT-based finite domain constraint solving. We introduce a tool called BEE (Ben-Gurion Equi-propagation Encoder) based on these ideas and demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

Recommendations

• Automatic generation of propagation complete SAT encodings
• meSAT: multiple encodings of CSP to SAT
• \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
• Efficient CNF encoding of Boolean cardinality constraints
• Theory and Applications of Satisfiability Testing

Cited in

(19)

• scientific article; zbMATH DE number 1696820 (Why is no real title available?)
• Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
• Characterizing Propagation Methods for Boolean Satisfiability
• scientific article; zbMATH DE number 2090309 (Why is no real title available?)
• SAT and IP based algorithms for magic labeling including a complete search for total magic labelings
• Breaking symmetries in graph search with canonizing sets
• Breaking symmetries with high dimensional graph invariants and their combination
• Theory and Applications of Satisfiability Testing
• Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)
• Complete symmetry breaking constraints for the class of uniquely Hamiltonian graphs
• Automatic generation of propagation complete SAT encodings
• Coupling different integer encodings for SAT
• Optimal-depth sorting networks
• scientific article; zbMATH DE number 1903342 (Why is no real title available?)
• aspartame: solving constraint satisfaction problems with answer set programming
• Sorting nine inputs requires twenty-five comparisons
• Compiling finite domain constraints to SAT with BEE
• \textit{clingcon}: the next generation
• Technology for translating combinatorial problems into Boolean equations

Describes a project that uses

Uses Software

• MINION

This page was built for publication: Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4913754)