Incremental Satisfiability Solving and its Applications

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.advisor Heljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland
dc.contributor.author Wieringa, Siert
dc.date.accessioned 2014-02-18T10:00:13Z
dc.date.available 2014-02-18T10:00:13Z
dc.date.issued 2014
dc.identifier.isbn 978-952-60-5569-5 (electronic)
dc.identifier.isbn 978-952-60-5568-8 (printed)
dc.identifier.issn 1799-4942 (electronic)
dc.identifier.issn 1799-4934 (printed)
dc.identifier.issn 1799-4934 (ISSN-L)
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/12600
dc.description.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. en
dc.format.extent 117 + app. 105
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Aalto University en
dc.publisher Aalto-yliopisto fi
dc.relation.ispartofseries Aalto University publication series DOCTORAL DISSERTATIONS en
dc.relation.ispartofseries 20/2014
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.subject.other Computer science en
dc.title Incremental Satisfiability Solving and its Applications en
dc.type G5 Artikkeliväitöskirja fi
dc.contributor.school Perustieteiden korkeakoulu fi
dc.contributor.school School of Science en
dc.contributor.department Tietotekniikan laitos fi
dc.contributor.department Department of Computer Science and Engineering en
dc.subject.keyword Incremental satisfiability solving en
dc.subject.keyword parallel satisfiability solving en
dc.subject.keyword applications of satisfiability solving en
dc.identifier.urn URN:ISBN:978-952-60-5569-5
dc.type.dcmitype text en
dc.type.ontasot Doctoral dissertation (article-based) en
dc.type.ontasot Väitöskirja (artikkeli) fi
dc.contributor.supervisor Heljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland
dc.opn Sakallah, Karem, prof., University of Michigan, Electrical Engineering and Computer Science, USA
dc.rev Marques-Silva, João, Prof., University College Dublin, Computer Science and Informatics, Ireland
dc.rev Sinz, Carsten, Dr. rer. nat., Karlsruhe Institute of Technology, Department of Mechanical Engineering, Germany
dc.date.defence 2014-03-14


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse