CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Translating Pseudo-Boolean Constraints into SAT

Niklas Een (Institutionen för data- och informationsteknik (Chalmers)) ; Niklas Sörensson
Journal on Satisfiability, Boolean Modeling and Computation, Special Volume on the SAT 2005 competitions and evaluations Editors: Daniel Le Berre and Laurent Simon (1574-0617). Vol. 2 (2005), p. 1-26.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: pseudo-Boolean, SAT-solver, SAT translation, integer linear programming

Denna post skapades 2008-09-24.
CPL Pubid: 74331


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik (Chalmers)
Institutionen för data- och informationsteknik, datavetenskap (GU) (GU)


Datavetenskap (datalogi)

Chalmers infrastruktur