@inproceedings{
    DBLP:conf/ecai/LaitinenJN10,
    editor = "Coelho, Helder and Studer, Rudi and Wooldridge, Michael",
    author = {Laitinen, Tero and Junttila, Tommi A. and Niemel{\"a}, Ilkka},
    volume = "215",
    title = "Extending Clause Learning {DPLL} with Parity Reasoning",
    url = "http://www.booksonline.iospress.nl/Content/View.aspx?piid=17707",
    series = "Frontiers in Artificial Intelligence and Applications",
    booktitle = "ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings",
    publisher = "IOS Press",
    corerank = "A",
    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.",
    responsibleauthor = "Laitinen, Tero",
    flags = "LOGIC MCM HIIT",
    year = "2010",
    unitcode = "T3060=99,U9014=1",
    impactfactor = "A4",
    pages = "21-26"
}