A Compact Reformulation of Propositional Satisfiability as Binary Constraint Satisfaction

Reference:

Matti Järvisalo and Ilkka Niemelä. A compact reformulation of propositional satisfiability as binary constraint satisfaction. In Alan M. Frisch and Ian Miguel, editors, Proceedings of the 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems: Towards Systemisation and Automation, pages 111–124, 2004. Proceedings available at http://www-users.cs.york.ac.uk/%7Efrisch/Reformulation/04/.

Abstract:

A binary CSP encoding for the propositional satisfiability problem (SAT) is introduced. To our knowledge, our encoding is the first one that is linear in the number of variables, domain size and constraint size w.r.t. the size of the SAT instance. Nevertheless, our encoding has the same properties as the well-known hidden variable encoding when comparing the performance of (i) the Davis-Putnam procedure with the Forward Checking and Maintaining Arc Consistency algorithms on the encoding, and (ii) the local search methods WalkSAT and GSAT with the Min Conflicts algorithm. Moreover, considering 2-SAT, it is shown that a generalisation of Papadimitriou's Random Walk algorithm has a quadratic expected running time on our encoding.

Suggested BibTeX entry:

@inproceedings{JN:Reform04,
    author = {Matti J{\"a}rvisalo and Ilkka Niemel{\"a}},
    booktitle = {Proceedings of the 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems: Towards Systemisation and Automation},
    editor = {Alan M. Frisch and Ian Miguel},
    note = {Proceedings available at \url{http://www-users.cs.york.ac.uk/\%7Efrisch/Reformulation/04/}},
    pages = {111--124},
    title = {A Compact Reformulation of Propositional Satisfiability as Binary Constraint Satisfaction},
    year = {2004},
}