Incremental Satisfiability Solving and its Applications

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
School of Science | Doctoral thesis (article-based) | Defence date: 2014-03-14
Checking the digitized thesis and permission for publishing
Instructions for the author
Date
2014
Department
Tietotekniikan laitos
Department of Computer Science and Engineering
Major/Subject
Mcode
Degree programme
Language
en
Pages
117 + app. 105
Series
Aalto University publication series DOCTORAL DISSERTATIONS, 20/2014
Abstract
The 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.
Description
Supervising professor
Heljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland
Thesis advisor
Heljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland
Keywords
Incremental satisfiability solving, parallel satisfiability solving, applications of satisfiability solving
Other note
Parts
  • [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.
  • [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.
  • [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.
  • [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.
  • [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.
  • [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.
Citation