id: 05887205
dt: a
an: 05887205
au: Laitinen, Tero; Junttila, Tommi; Niemelä, Ilkka
ti: Extending clause learning DPLL with parity reasoning.
so: Coelho, Helder (ed.) et al., ECAI 2010. 19th European conference on
    artificial intelligence, August 16‒20, 2010 Lisbon, Portugal.
    Including proceedings of the 6th prestigious applications of artificial
    intelligence (PAIS-2010). Amsterdam: IOS Press (ISBN
    978-1-60750-605-8/pbk; 978-1-60750-606-5/ebook). Frontiers in
    Artificial Intelligence and Applications 215, 21-26 (2010).
py: 2010
pu: Amsterdam: IOS Press
la: EN
cc: 
ut: 
ci: 
li: doi:10.3233/978-1-60750-606-5-21
ab: Summary: 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 detection 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.
rv: