Extending SAT Solver with Parity Reasoning

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.advisorJunttila, Tommi, Docent, Aalto University, Department of Information and Computer Science, Finland
dc.contributor.authorLaitinen, Tero
dc.contributor.departmentTietojenkäsittelytieteen laitosfi
dc.contributor.departmentDepartment of Information and Computer Scienceen
dc.contributor.schoolPerustieteiden korkeakoulufi
dc.contributor.schoolSchool of Scienceen
dc.contributor.supervisorNiemelä, Ilkka, Prof., Aalto University, Department of Information and Computer Science, Finland
dc.date.accessioned2014-11-04T10:00:29Z
dc.date.available2014-11-04T10:00:29Z
dc.date.defence2014-11-21
dc.date.issued2014
dc.description.abstractPropositional conflict-driven clause-learning (CDCL) satisfy ability (SAT) solvers have been successfully applied in a number of industrial domains. In some application areas such as circuit verification, bounded model checking, logical cryptanalysis, and approximate model counting, some requirements can be succinctly captured with parity (xor) constraints. However, satisfy ability solvers that typically operate in conjunctive normal form (CNF) may perform poorly with straightforward translation of parity constraints to CNF. This work studies how CDCL SAT solvers can be enhanced to handle problems with parity constraints using the recently introduced DPLL (XOR) framework where the SAT solver is coupled with a parity constraint solver module. Different xor-deduction systems ranging from plain unit propagation through equivalence reasoning to complete incremental Gauss-Jordan elimination are presented. Techniques to analyze xor-deduction system derivations are developed, allowing one to obtain smaller clausal explanations for implied literals and also to learn new parity constraints in the conflict analysis process. It is proven that these techniques can be used to simulate a complete xor-deduction system on a restricted class of instances and allow very short unsatisfiability proofs for some formulas whose CNF translations are hard for resolution. Fast approximating tests to detect whether unit propagation or equivalence reasoning is enough to deduce all implied literals are presented. Methods to decompose sets of parity constraints into sub problems that can be handled separately are developed. The decomposition methods can greatly reduce the size of parity constraint matrices when using Gauss-Jordan elimination on dense matrices and allow one to choose appropriate xor-deduction system for each sub problem. Efficient translations to simulate equivalence reasoning and stronger parity reasoning are developed. It is shown that equivalence reasoning can be simulated by adding a polynomial amount of redundant parity constraints to the problem, but without using additional variables, an exponential number of parity constraints are needed in the worst case. It is proven that resolution simulates equivalence reasoning efficiently. The presented techniques are experimentally evaluated on a variety of challenging problems originating from a number of encryption ciphers and from SAT Competition benchmark instances.en
dc.description.abstractHakukonflikteista oppivia lauselogiikan toteutuvuustarkastimia on menestyksekkäästi sovellettu ongelmanratkaisuun useissa käytännön sovellutuksissa. Tietyillä sovellusalueilla, kuten piiriverifiointi, rajoitettu mallintarkastus, looginen kryptoanalyysi ja approksimoiva ratkaisumallien lukumäärän laskenta, ongelmakuvauksien vaatimuksia voidaan ilmaisuvoimaisesti mallintaa pariteettirajoitteilla. Ongelmat, jotka sisältävät pariteetti- eli xor-rajoitteita, voivat tosin olla erityisen vaativia toteutuvuustarkistimille, jotka käsittelevät ongelmaa konjunktiivisessa normaalimuodossa. Tässä väitöskirjassa tutkitaan, miten hakukonflikteista oppivia toteutuvuustarkistimia voidaan kehittää käsittelemään pariteettirajoitteita sisältäviä ongelmia käyttäen aikaisemmin julkaistua DPLL(XOR)-hakumenetelmäkehystä, jossa toteutuvuustarkistimeen yhdistetään pariteettirajoitteita käsittelevä ratkaisinmoduuli. Työssä esitellään erilaisia pariteettipäättelyjärjestelmiä kuten yksikköpropagaatio, ekvivalenssipäättely ja täydellisen pariteettipäättelyn tuottava inkrementaalinen Gauss-Jordan-eliminaatio. Pariteettirajoitejohtoihin perustuvien pariteettipäättelyjärjestelmien analysoimiseksi esitellään tekniikoita, joilla voidaan johtaa lyhyempiä klausuulipohjaisia selityksiä implikoiduille literaaleille ja joita voidaan käyttää uusien pariteettirajoitteiden oppimiseksi hakukonfliktien käsittelyn yhteydessä. Työssä osoitetaan, että näillä tekniikoilla voidaan simuloida täydellistä pariteettipäättelyjärjestelmää rajatussa ongelmajoukossa ja niiden avulla voidaan tuottaa lyhyitä ongelman toteutumattomuuden osoittavia todistuksia eräille ongelmille, joiden kuvaukset konjunktiivisessa normaalimuodossa ovat vaikeita resoluutiolle. Väitöskirjassa käsitellään approksimoivia luokittelumenetelmiä, joilla voidaan päätellä, että annetulle ongelmalle riittää käyttää yksikköpropagaatiota tai ekvivalenssipäättelyä kaikkien implikoitujen literaalien päättelyyn. Työssä näytetään, miten erilaisia menetelmiä osittaa ongelma erillisiksi aliongelmiksi voidaan soveltaa pariteettirajoitejoukkoihin. Ositusmenetelmiä voidaan käyttää pienentämään Gauss-Jordan eliminaatiossa käytettävien matriisien kokoa, kun käytetään tiivistä matriisiesitystä, ja jokaiselle ositetulle aliongelmalle voidaan valita sopiva pariteettipäättelyjärjestelmä. Pariteettipäättelyn simulointia tutkitaan käyttäen ekvivalenssipäättelyä ja vahvempaa pariteettipäättelyä simuloivia käännöksiä, jotka mahdollistavat olemassa olevien toteutuvuustarkistimien hyödyntämisen. Työssä osoitetaan, että ekvivalenssipäättelyä voidaan simuloida lisäämällä polynominen määrä ylimääräisiä pariteettirajoitteita, mutta ilman lisämuuttujia tarvitaan eksponentiaalinen määrä pariteettirajoitteita pahimmassa tapauksessa. Työssä näytetään, että resoluutio simuloi ekvivalenssipäättelyä tehokkaasti. Esiteltyjä tekniikoita arvioidaan kokeellisesti monilla haastavilla ongelmilla, jotka on tuotettu salausmenetelmistä ja SAT Competitionkilpailuongelmista.fi
dc.format.extent151 + app. 78
dc.format.mimetypeapplication/pdfen
dc.identifier.isbn978-952-60-5945-7 (electronic)
dc.identifier.isbn978-952-60-5944-0 (printed)
dc.identifier.issn1799-4942 (electronic)
dc.identifier.issn1799-4934 (printed)
dc.identifier.issn1799-4934 (ISSN-L)
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/14418
dc.identifier.urnURN:ISBN:978-952-60-5945-7
dc.language.isoenen
dc.opnBiere, Armin, Prof., Johannes Kepler University, Austria
dc.publisherAalto Universityen
dc.publisherAalto-yliopistofi
dc.relation.haspart[Publication 1]: Tero Laitinen and Tommi Junttila and Ilkka Niemelä. Equivalence Class Based Parity Reasoning in DPLL(XOR). In IEEE 23rd International Conference on Tools with Artificial Intelligence, ICTAI 2011, Boca Raton, FL, USA, November 7-9, 2011, 649-658, November 2011. DOI: 10.1109/ICTAI.2011.103
dc.relation.haspart[Publication 2]: Tero Laitinen and Tommi Junttila and Ilkka Niemelä. Conflict-Driven XOR-Clause Learning. In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012, 383-396, June 2012. DOI: 10.1007/978-3-642-31612-8_29
dc.relation.haspart[Publication 3]: Tero Laitinen and Tommi Junttila and Ilkka Niemelä. Classifying and Propagating Parity Constraints. In Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012, 357-372, October 2012. DOI: 10.1007/978-3-642-33558-7_28
dc.relation.haspart[Publication 4]: Tero Laitinen and Tommi Junttila and Ilkka Niemelä. Extending Clause Learning SAT Solvers with Complete Parity Reasoning. In IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9, 2012, 65-72, November 2012. DOI: 10.1109/ICTAI.2012.18
dc.relation.haspart[Publication 5]: Tero Laitinen and Tommi Junttila and Ilkka Niemelä. Simulating Parity Reasoning. In 19th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Stellenbosch, South Africa, December 15-19, 2013, 568-583, December 2013. DOI: 10.1007/978-3-642-45221-5_38
dc.relation.ispartofseriesAalto University publication series DOCTORAL DISSERTATIONSen
dc.relation.ispartofseries177/2014
dc.revLi, Chu Min, prof., Université de Picardie Jules Verne, France
dc.revSebastiani, Roberto, prof., University of Trento, Italy
dc.subject.keywordpropositional satisfiabilityen
dc.subject.keywordparity reasoningen
dc.subject.keywordlauselogiikan toteutuvuusongelmafi
dc.subject.keywordpariteettipäättelyfi
dc.subject.otherComputer scienceen
dc.titleExtending SAT Solver with Parity Reasoningen
dc.titleLauselogiikan toteutuvuustarkistimen laajentaminen pariteettipäättelylläfi
dc.typeG5 Artikkeliväitöskirjafi
dc.type.dcmitypetexten
dc.type.ontasotDoctoral dissertation (article-based)en
dc.type.ontasotVäitöskirja (artikkeli)fi
local.aalto.digiauthask
local.aalto.digifolderAalto_66881
Files
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
isbn9789526059457.pdf
Size:
2.02 MB
Format:
Adobe Portable Document Format