Extending Clause Learning SAT Solvers with Complete Parity Reasoning

Tero Laitinen*, Tommi Junttila, Ilkka Niemelä

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

    10 Citations (Scopus)


    Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instance is a combination of traditional clauses and parity constraints. This paper studies how such combined problems can be efficiently solved by augmenting a modern SAT solver with an xor-reasoning module in the DPLL(XOR) framework. A new xor-reasoning module that deduces all possible implied literals using incremental Gauss-Jordan elimination is presented. A decomposition technique that can greatly reduce the size of parity constraint matrices while still allowing to deduce all implied literals is presented. It is shown how to eliminate variables occuring only in parity constraints while preserving the decomposition. The proposed techniques are evaluated experimentally.

    Original languageEnglish
    Title of host publication2012 IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012
    Number of pages8
    ISBN (Print)978-1-4799-0227-9, 9780769549156
    Publication statusPublished - 2012
    MoE publication typeA4 Article in a conference publication
    EventIEEE International Conference on Tools with Artificial Intelligence - Athens, Greece
    Duration: 7 Nov 20129 Nov 2012
    Conference number: 24

    Publication series

    NameProceedings-International Conference on Tools With Artificial Intelligence
    ISSN (Print)1082-3409


    ConferenceIEEE International Conference on Tools with Artificial Intelligence
    Abbreviated titleICTAI


    • DPLL(T)


    Dive into the research topics of 'Extending Clause Learning SAT Solvers with Complete Parity Reasoning'. Together they form a unique fingerprint.

    Cite this