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