Eén, Niklas; Sörensson, Niklas Translating pseudo-Boolean constraints into SAT. (English) Zbl 1116.68083 J. Satisf. Boolean Model. Comput. 2, No. 1-4, 1-26 (2006). Summary: 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. Cited in 3 ReviewsCited in 76 Documents MSC: 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) Keywords:SAT translation; integer linear programming; SAT-solver Software:MiniSat PDFBibTeX XMLCite \textit{N. Eén} and \textit{N. Sörensson}, J. Satisf. Boolean Model. Comput. 2, No. 1--4, 1--26 (2006; Zbl 1116.68083)