Learning Centre

Extending SAT solver with parity constraints

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Laitinen, Tero
dc.date.accessioned 2011-11-28T13:26:16Z
dc.date.available 2011-11-28T13:26:16Z
dc.date.issued 2010
dc.identifier.isbn 978-952-60-3224-5
dc.identifier.issn 1797-5042
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/910
dc.description.abstract Current methods for solving Boolean satisfiability problem (SAT) are scalable enough to solve discrete nonlinear problems involving hundreds of thousands of variables. However, modern SAT solvers scale poorly with problems involving parity constraints (linear equations modulo 2). Gaussian elimination can be used to solve a system of linear equation effectively but it cannot be applied as such when the problem description also contains nonlinear constraints. A SAT solver typically reads the problem description in conjunctive normal form (CNF). Representing parity constraints in CNF results in an inefficient encoding which partly makes solving the problem harder. Also, the deduction methods used in SAT solvers are not efficient when solving problems involving parity constraints. This report develops an efficient xor-reasoning module for deciding the satisfiability of a conjunction of parity constraints and studies alternative ways to integrate the xor-reasoning module into a modern conflict-driven clause learning SAT solver. The novelty of the approach is the combination of conflict-driven clause learning techniques (CDCL) with equivalence reasoning enhancing deduction capabilities of CDCL SAT solvers beyond unit propagation on the CNF formula. The presented proof system and the abstract model for computing clausal explanations for inconsistent valuations of variables allow for different possible implementations. Key design principles along with alternative ways to compute clausal explanations and to integrate the xor-reasoning module into a SAT solver are presented, analyzed, and compared. We have integrated the xor-reasoning module into a state-of-the-art CDCL SAT solver, minisat. The applicability of the hybrid approach is evaluated experimentally and compared with a number of modern SAT solvers on three challenging benchmarks: randomly generated regular linear problems, a known keystream attack on the stream cipher Trivium, and a known plaintext attack on the block cipher DES. The results are promising: the number of heuristics decisions needed typically decreases without causing unbearable computational overhead. Larger problem instances may even be solved faster by minisat with the xor-reasoning module than by the unmodified version. en
dc.format.extent 73
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Aalto University School of Science and Technology en
dc.publisher Aalto-yliopiston teknillinen korkeakoulu fi
dc.relation.ispartofseries TKK reports in information and computer science en
dc.relation.ispartofseries 32 en
dc.subject.other Computer science en
dc.title Extending SAT solver with parity constraints en
dc.contributor.school Faculty of Information and Natural Sciences en
dc.contributor.school Informaatio- ja luonnontieteiden tiedekunta fi
dc.contributor.department Department of Information and Computer Science en
dc.contributor.department Tietojenkäsittelytieteen laitos fi
dc.subject.keyword SAT en
dc.subject.keyword Boolean logic en
dc.subject.keyword parity constraint en
dc.subject.keyword conflict-driven en
dc.identifier.urn urn:nbn:fi:tkk-013150
dc.type.dcmitype text en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication