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

DOI10.1613/JAIR.3809zbMATH Open1267.68216arXiv1402.0568OpenAlexW3102811762WikidataQ129493544 ScholiaQ129493544MaRDI QIDQ4913754FDOQ4913754

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)

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.

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

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

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)

Cited In (19)

• Title not available (Why is that?)
• Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
• Characterizing Propagation Methods for Boolean Satisfiability
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• 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

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)