search query: @keyword SAT / total: 6
reference: 2 / 6
| Author: | Laitinen, Tero Olavi |
| Title: | Extending SAT solver with parity constraints |
| Lauselogiikan toteutuvuustarkistimen laajentaminen lineaariyhtälöillä (modulo 2) | |
| Publication type: | Master's thesis |
| Publication year: | 2010 |
| Pages: | vi + 73 Language: eng |
| Department/School: | Informaatio- ja luonnontieteiden tiedekunta |
| Main subject: | Tietojenkäsittelyteoria (T-119) |
| Supervisor: | Niemelä, Ilkka |
| Instructor: | Junttila, Tommi |
| OEVS: | Electronic archive copy is available via Aalto Thesis Database.
Instructions Reading digital theses in the closed network of the Aalto University Harald Herlin Learning CentreIn the closed network of Learning Centre you can read digital and digitized theses not available in the open network. The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/ You can read theses on the Learning Centre customer computers, which are available on all floors.
Logging on to the customer computers
Opening a thesis
Reading the thesis
Printing the thesis
|
| Location: | P1 Ark Aalto | Archive |
| Keywords: | SAT Boolean logic parity constraint conflict-driven SAT Boolen logiikka lineaariyhtälö (mod 2) konfliktioppiminen |
| Abstract (eng): | 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 he 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 thesis 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-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. |
| Abstract (fin): | Lauselogiikan toteutuvuusongelmaa (SAT-ongelma) varten kehitetyt tehokkaat ratkaisumenetelmät soveltuvat suurten epälineaarisia komponentteja sisältävien diskreettien ongelmien ratkaisuun. Lineaaristen ongelmien ratkaisuun on tehokkaampia menetelmiä mutta näitä ei voi suoraan käyttää, jos ongelmakuvauksessa on lisäksi epälineaarisia rajoitteita. Lauselogiikan toteutuvuusongelman ratkaisin (SAT-ratkaisin) edellyttää, että ongelmakuvaus on konjunktiivisessa normaalimuodossa. Lineaarisen ongelman esittäminen konjunktiivisessa normaalimuodossa kasvattaa ongelmakuvauksen kokoa muuttujien tai rajoitteiden lukumäärän suhteen, mikä tekee ongelman ratkaisemisesta laskennallisesti vaativampaa. Lisäksi SAT-ratkaisimissa käytetyt päättelymenetelmät eivät ole tehokkaita lineaaristen ongelmien ratkaisemiseen. Tässä diplomityössä tutkitaan SAT-ratkaisimien laajentamista lineaaristen totuusarvoyhtälöiden teoriamoduulilla, jolle annetaan ratkaistavan toteutuvuusongelman lineaarinen osa sellaisenaan. Lähestymistapa tarjoaa uuden menetelmän yhdistää ekvivalenssipäättely ja konflikteihin perustuva klausuulien oppiminen SAT-ratkaisimessa. Teoriamoduulin todistusjärjestelmä ja abstrakti malli SAT-ratkaisimessa hyödynnettävistä klausuulimuotoisista konfliktien selityksistä toimivat perustana teoriamoduulin monille mahdollisille implementaatioille. Diplomityössä kuvataan ja analysoidaan tärkeimpien suunnitteluperiaatteiden lisäksi erilaisia tapoja laskea klausuulipohjaisia selityksiä konflikteille ja integroida teoriamoduuli SAT-ratkaisimeen. Teoriamoduuli on integroitu tehokkaaseen konfliktioppivaan SAT-ratkaisimeen (minisat). Yhdistetyn menetelmän soveltuvuutta tutkitaan satunnaisesti tuotettujen lineaaristen ongelmien kanssa sekä kryptoanalyysin työkaluna tutkimuskohteina jonosalain Trivium ja lohkosalain DES. Tulokset ovat lupaavia: ratkaisussa tarvittavien heurististen päätöksien lukumäärä tyypillisesti vähenee aiheuttamatta kohtuuttomasti ylimääräistä laskentaa. Isompien ongelmainstanssien ratkaisuun tarvittava aika on yhdistetyllä menetelmällä ajoittain jopa lyhyempi kuin minisat-ratkaisimella teoriamoduulin ansiosta. |
| ED: | 2010-07-09 |
INSSI record number: 39880
+ add basket
INSSI