Extending Clause Learning SAT Solvers with Complete Parity Reasoning

Tero Laitinen*, Tommi Junttila, Ilkka Niemelä

*Tämän työn vastaava kirjoittaja

    Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

    10 Sitaatiot (Scopus)

    Abstrakti

    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.

    AlkuperäiskieliEnglanti
    Otsikko2012 IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012
    KustantajaIEEE
    Sivut65-72
    Sivumäärä8
    Vuosikerta1
    ISBN (painettu)978-1-4799-0227-9, 9780769549156
    DOI - pysyväislinkit
    TilaJulkaistu - 2012
    OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
    TapahtumaIEEE International Conference on Tools with Artificial Intelligence - Athens, Kreikka
    Kesto: 7 marrask. 20129 marrask. 2012
    Konferenssinumero: 24

    Julkaisusarja

    NimiProceedings-International Conference on Tools With Artificial Intelligence
    KustantajaIEEE
    ISSN (painettu)1082-3409

    Conference

    ConferenceIEEE International Conference on Tools with Artificial Intelligence
    LyhennettäICTAI
    Maa/AlueKreikka
    KaupunkiAthens
    Ajanjakso07/11/201209/11/2012

    Sormenjälki

    Sukella tutkimusaiheisiin 'Extending Clause Learning SAT Solvers with Complete Parity Reasoning'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

    Siteeraa tätä