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

Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential

Matti Järvisalo

Dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the Faculty of Information and Natural Sciences for public examination and debate in Auditorium T2 at Helsinki University of Technology (Espoo, Finland) on the 29th of November, 2008, at 10 o'clock.

Overview in PDF format (ISBN 978-951-22-9642-2)   [1857 KB]
Dissertation is also available in print (ISBN 978-951-22-9641-5)

Abstract

Constraint satisfaction deals with developing automated techniques for solving computationally hard problems in a declarative fashion. The main emphasis of this thesis is on constraint satisfaction techniques for the propositional satisfiability problem (SAT).

As solving techniques for propositional satisfiability have rapidly progressed during the last 15 years, implementations of decision procedures for SAT, so called SAT solvers, have been found to be extremely efficient as back-end search engines in solving large industrial-scale combinatorial problems. Since SAT solvers have become a standard tool for solving various real-world problem instances of increasing size and difficulty, there is a demand for more and more robust and efficient solvers. For understanding the success (and failures) of SAT solving in specific problem domains, it is important to investigate how different types of structural properties of SAT instances are related to the efficiency of solving the instances with different SAT-based constraint satisfaction techniques. This is the underlying motivation for this thesis.

The emphasis of the thesis is on search-based SAT solving techniques for solving structured real-world problems. The work focuses on selected topics related to the analysis and development of both complete and stochastic local search methods for SAT. Both experimental and proof complexity theoretic approaches are applied. The main contributions are three-fold.

The work contributes to the analysis of structure-based branching heuristics. A proof complexity theoretic power hierarchy is established for DPLL and clause learning SAT solvers with various structure-based branching restrictions. The proof complexity theoretic results are complemented by a detailed experimental evaluation of the effects of structure-based branching on state-of-the-art SAT solvers. In connection with structure-based branching in SAT, the work introduces the Extended ASP Tableaux proof system in the context of answer set programming, which is a field closely related to SAT solving.

The work also contributes to the development of stochastic local search methods for structured real-world SAT instances. A novel non-clausal local search method for SAT is developed by incorporating the concept of justification frontiers previously applied in the context of complete non-clausal solvers. Variants of the method are analyzed with respect approximate completeness, and adaptive noise mechanisms aimed specifically for the method are developed.

As a third point of view to structure in SAT, the work addresses the problem of generating hard satisfiable SAT instances for both DPLL-based and local search solvers by introducing the regular XORSAT model. Additionally, techniques for applying XORSAT instances specifically for benchmarking equivalence reasoning techniques in SAT solvers are developed.

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

  1. Harri Haanpää, Matti Järvisalo, Petteri Kaski, and Ilkka Niemelä. 2006. Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. Journal on Satisfiability, Boolean Modeling and Computation, volume 2, numbers 1-4, pages 27-46. © 2006 Delft University of Technology. By permission.
  2. Matti Järvisalo and Ilkka Niemelä. 2008. The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study. Journal of Algorithms: Algorithms in Cognition, Informatics and Logic, volume 63, numbers 1-3, pages 90-113. © 2008 Elsevier Science. By permission.
  3. Matti Järvisalo and Tommi Junttila. 2008. Limitations of restricted branching in clause learning. Constraints, to appear, 29 pages. © 2008 by authors and © 2008 Springer Science+Business Media. By permission.
  4. Matti Järvisalo and Tommi Junttila. 2008. On the power of top-down branching heuristics. In: Dieter Fox and Carla P. Gomes (editors). Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008). Chicago, Illinois, USA. 13-17 July 2008. AAAI Press, pages 304-309.
  5. Matti Järvisalo and Emilia Oikarinen. 2008. Extended ASP tableaux and rule redundancy in normal logic programs. Theory and Practice of Logic Programming, volume 8, numbers 5-6, pages 691-716.
  6. Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. 2008. Justification-based non-clausal local search for SAT. In: Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos Avouris (editors). Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008). Patras, Greece. 21-25 July 2008. IOS Press. Frontier in Artificial Intelligence and Applications, volume 178, pages 535-539. © 2008 IOS Press. By permission.
  7. Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. 2008. Justification-based local search with adaptive noise strategies. In: Iliano Cervesato, Helmut Veith, and Andrei Voronkov (editors). Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008). Doha, Qatar. 22-27 November 2008. Springer. Lecture Notes in Computer Science, volume 5330, pages 31-46. © 2008 Springer Science+Business Media. By permission.

Keywords: propositional satisfiability, SAT, clause learning, DPLL, stochastic local search, branching heuristics, proof complexity, Boolean circuits, non-clausal formulas, problem structure, backdoors, hard instances, adaptive noise strategies, probabilistically approximately complete, answer set programming

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

© 2008 Helsinki University of Technology

Last update 2011-05-26