Incremental Satisfiability Solving and its Applications

Simple item page
dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.advisorHeljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland 
dc.contributor.authorWieringa, Siert 
dc.contributor.departmentTietotekniikan laitosfi
dc.contributor.departmentDepartment of Computer Science and Engineeringen
dc.contributor.schoolPerustieteiden korkeakoulufi
dc.contributor.schoolSchool of Scienceen
dc.contributor.supervisorHeljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland 
dc.date.accessioned2014-02-18T10:00:13Z
dc.date.available2014-02-18T10:00:13Z
dc.date.defence2014-03-14 
dc.date.issued2014 
dc.description.abstractThe propositional logic satisfiability problem (SAT) is a computationally hard decision problem. Despite its theoretical hardness, decision procedures for solving instances of this problem have become surprisingly efficient in recent years. These procedures, known as SAT solvers, are able to solve large instances originating from real-life problem domains, such as artificial intelligence and formal verification. Such real-life applications often require solving several related instances of SAT. Therefore, modern solvers posses an incremental interface that allows the input of sequences of incrementally encoded instances of SAT. When solving these instances sequentially the solver can reuse some of the information it has gathered across related consecutive instances. This dissertation contains six publications. The two focus areas of the combined work are incremental usage of SAT solvers, and the usage of parallelism in applications of SAT solvers. It is shown in this work that these two seemingly contradictory concepts form a natural combination. Moreover, this dissertations unifies, analyzes, and extends the results of the six publications, for example, by studying information propagation in incremental solvers through graphical visualizations. The concrete contributions made by the work in this dissertation include, but are not limited to: Improvements to algorithms for MUS finding, the use of graphical visualizations to understand information propagation in incremental solvers, asynchronous incremental solving, and concurrent clause strengthening.en
dc.format.extent117 + app. 105 
dc.format.mimetypeapplication/pdf 
dc.identifier.isbn978-952-60-5569-5 (electronic) 
dc.identifier.isbn978-952-60-5568-8 (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/12600
dc.identifier.urnURN:ISBN:978-952-60-5569-5 
dc.language.isoenen
dc.opnSakallah, Karem, prof., University of Michigan, Electrical Engineering and Computer Science, USA 
dc.publisherAalto Universityen
dc.publisherAalto-yliopistofi
dc.relation.haspart[Publication 1]: Hans van Maaren and Siert Wieringa. Finding Guaranteed MUSes Fast. In Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, volume 4996, pages 291-304. Guangzhou, China, May 2008. 
dc.relation.haspart[Publication 2]: Siert Wieringa. On Incremental Satisfiability and Bounded Model Checking. In Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), CEUR workshop proceedings, volume 832, pages 46-54. Workshop affiliated to the 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, Texas, November 2011. 
dc.relation.haspart[Publication 3]: Marijn J.H. Heule and Oliver Kullmann and Siert Wieringa and Armin Biere. Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In Revised Selected Papers of the 7th international Haifa Verification Conference (HVC), Lecture Notes in Computer Science, volume 7261, pages 50-65. Haifa, Israel, December 2011, published 2012. 
dc.relation.haspart[Publication 4]: Siert Wieringa. Understanding, Improving and Parallelizing MUS Finding Using Model Rotation. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming CP), Lecture Notes in Computer Science, volume 7514, pages 672-687. Québec City, Canada, October 2012. 
dc.relation.haspart[Publication 5]: Siert Wieringa and Keijo Heljanko. Asynchronous Multi-core Incremental SAT Solving. In Proceedings of the 19th international conference on Tools and Algorithms for the Construction of Analysis of Systems (TACAS), Lecture Notes in Computer Science, volume 7795, pages 139-153. Held as part of European Joint Conferences on Theory and Applications of Software (ETAPS), Rome, Italy, March 2013. 
dc.relation.haspart[Publication 6]: Siert Wieringa and Keijo Heljanko. Concurrent Clause Strengthening. In Proceedings of the 16th international conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, volume 7962, pages 116-132. Helsinki, Finland, July 2013. 
dc.relation.ispartofseriesAalto University publication series DOCTORAL DISSERTATIONSen
dc.relation.ispartofseries20/2014 
dc.revMarques-Silva, João, Prof., University College Dublin, Computer Science and Informatics, Ireland 
dc.revSinz, Carsten, Dr. rer. nat., Karlsruhe Institute of Technology, Department of Mechanical Engineering, Germany 
dc.subject.keywordIncremental satisfiability solvingen
dc.subject.keywordparallel satisfiability solvingen
dc.subject.keywordapplications of satisfiability solvingen
dc.subject.otherComputer scienceen
dc.titleIncremental Satisfiability Solving and its Applicationsen
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_67849
Files
Original bundle
Now showing 1 - 3 of 3
No Thumbnail Available
Name:
isbn9789526055695.pdf
Size:
3.7 MB
Format:
Adobe Portable Document Format
Download
No Thumbnail Available
Name:
errata_of_P1_PIV.pdf
Size:
36.86 KB
Format:
Adobe Portable Document Format
Download
No Thumbnail Available
Name:
publication2.pdf
Size:
244.79 KB
Format:
Adobe Portable Document Format
Description:
Download
Collections
[diss] Perustieteiden korkeakoulu / SCI