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

    5 Citations (Scopus)

    Abstract

    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
    PublisherIEEE
    Pages65-72
    Number of pages8
    Volume1
    ISBN (Print)978-1-4799-0227-9, 9780769549156
    DOIs
    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
    PublisherIEEE
    ISSN (Print)1082-3409

    Conference

    ConferenceIEEE International Conference on Tools with Artificial Intelligence
    Abbreviated titleICTAI
    CountryGreece
    CityAthens
    Period07/11/201209/11/2012

    Keywords

    • DPLL(T)

    Cite this