Grid based propositional satisfiability solving

Thumbnail Image
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu | Doctoral thesis (article-based)
Checking the digitized thesis and permission for publishing
Instructions for the author
Degree programme
Verkkokirja (1732 KB, 97 s.)
Aalto University publication series DOCTORAL DISSERTATIONS , 118/2011
This work studies how grid and cloud computing can be applied to efficiently solving propositional satisfiability problem (SAT) instances. Propositional logic provides a convenient language for expressing real-world originated problems such as AI planning, automated test pattern generation, bounded model checking and cryptanalysis. The interest in SAT solving has increased mainly due to improvements in the solving algorithms, which recently have increasingly focused on using parallelism offered by multi-CPU computers. Partly orthogonally to these improvements this work studies several novel approaches to parallel solving of SAT instances in a grid of widely distributed "virtual" computers instead of workstations or supercomputers. Two types of parallel SAT solving approaches are analyzed and used as building blocks for more complex systems: using several solvers which compete to solve a given instance in parallel, and splitting the search space of the instance and solving the resulting partitions in parallel. The work presents several efficient partitioning functions, critical in successful splitting according to an analytical result, and presents novel solving systems that are less dependent on the partitioning function efficiency. Finally, the work studies combining clause learning, a key technique in modern SAT solvers, with the novel types of parallel solvers. Different heuristics are studied for filtering clauses learned in parallel, and the work proposes techniques which allow exchanging the clauses between different splits. The practical significance of the results are studied using large, standard benchmark sets from SAT competitions. Some of the approaches are able to solve several instances that have either not been solved at all by any other solver, or which are significantly slower to solve with other solvers.
Supervising professor
Niemelä, Ilkka, Prof.
Thesis advisor
Junttila, Tommi, Dr.
constraint based search, randomized search, propositional satisfiability problem, DPLL procedure, clause learning, parallel computing, cloud computing, grid computing
Other note
  • [Publication 1]: Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Strategies for Solving SAT in Grids by Randomized Search. In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2008), volume 5144 of Lecture Notes in Artificial Intelligence, pages 125-140, July/August 2008.
  • [Publication 2]: Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Incorporating Clause Learning in Grid-Based Randomized SAT Solving. Journal on Satisfiability, Boolean Modeling and Computation, volume 6, number 4, pages 223-244, June 2009.
  • [Publication 3]: Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning Search Spaces of a Randomized Search. Fundamenta Informaticae, volume 107, Number 2-3, pages 289-311, September 2011.
  • [Publication 4]: Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning SAT Instances for Distributed Solving. In Proceedings of the 17th international conference of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), volume 6397 of Lecture Notes in Computer Science, pages 372-386, October 2010.
  • [Publication 5]: Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Grid-Based SAT Solving with Iterative Partitioning and Clause Learning. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011), volume 6876 of Lecture Notes in Computer Science, pages 385-399, September 2011.