Title: | Incremental Satisfiability Solving and its Applications |
Author(s): | Wieringa, Siert |
Date: | 2014 |
Language: | en |
Pages: | 117 + app. 105 |
Department: | Tietotekniikan laitos Department of Computer Science and Engineering |
ISBN: | 978-952-60-5569-5 (electronic) 978-952-60-5568-8 (printed) |
Series: | Aalto University publication series DOCTORAL DISSERTATIONS, 20/2014 |
ISSN: | 1799-4942 (electronic) 1799-4934 (printed) 1799-4934 (ISSN-L) |
Supervising professor(s): | Heljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland |
Thesis advisor(s): | Heljanko, Keijo, Assoc. prof., Aalto University, Department of Computer Science and Engineering, Finland |
Subject: | Computer science |
Keywords: | Incremental satisfiability solving, parallel satisfiability solving, applications of satisfiability solving |
OEVS yes | |
|
|
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.
|
|
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. |
|
|
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Page content by: Aalto University Learning Centre | Privacy policy of the service | About this site