The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
Aalto

Grid Based Propositional Satisfiability Solving

Antti E. J. Hyvärinen

Doctoral dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the School of Science for public examination and debate in Auditorium T2 at the Aalto University School of Science (Espoo, Finland) on the 28th of November 2011 at 12 noon.

Overview in PDF format (ISBN 978-952-60-4368-5)   [1732 KB]
Dissertation is also available in print (ISBN 978-952-60-4367-8)

Abstract

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.

This thesis consists of an overview and of the following 5 publications:

  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.
  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.
  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.
  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.
  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.

Keywords: constraint based search, randomized search, propositional satisfiability problem, DPLL procedure, clause learning, parallel computing, cloud computing, grid computing

This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.

© 2011 Aalto University

Last update 2011-11-24