Extending Clause Learning DPLL with Parity Reasoning

Reference:

Tero Laitinen, Tommi A. Junttila, and Ilkka Niemelä. Extending clause learning DPLL with parity reasoning. In Helder Coelho, Rudi Studer, and Michael Wooldridge, editors, ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 21–26. IOS Press, 2010.

Abstract:

We consider a combined satisfiability problem where an instance is given in two parts: a set of traditional clauses extended with a set of parity (xor) constraints. To solve such problems without translation to CNF, we develop a parity constraint reasoning method that can be integrated to a clause learning solver. The idea is to devise a module that offers a decision procedure and implied literal detec- tion for parity constraints and also provides clausal explanations for implied literals and conflicts. We have implemented the method and integrated it to a state-of-the-art clause learning solver. The resulting system is experimentally evaluated and compared to state-of-the-art solvers.

Suggested BibTeX entry:

@inproceedings{tolaiti2.DBLP:confecaiLaitinenJN10,
    author = {Tero Laitinen and Tommi A. Junttila and Ilkka Niemel{\"a}},
    booktitle = {ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings},
    editor = {Helder Coelho and Rudi Studer and Michael Wooldridge},
    pages = {21-26},
    publisher = {IOS Press},
    series = {Frontiers in Artificial Intelligence and Applications},
    title = {Extending Clause Learning {DPLL} with Parity Reasoning},
    volume = {215},
    year = {2010},
}