HIIT seminar, Friday Oct 9, 10:15 a.m. (coffee from 10), Exactum D122
Dr. Matti Järvisalo
University of Helsinki
Department of Computer Science
On the Power of Structure-Based Decision Heuristics for SAT
Abstract:
Constraint reasoning techniques based on Boolean satisfiability (SAT) have proven extremely effective for solving hard, industrially relevant combinatorial problems in domains such as hardware and software verification and AI planning. In the SAT-based approaches, a problem is encoded in propositional logic, and this declarative specification is then solved using general-purpose SAT solvers.
Understanding the effect of the inherent structural properties of real-world SAT instances is considered a key aspect in developing increasingly efficient and robust SAT solvers. Complete, DPLL-style SAT solvers are the most efficient ones for real-world applications today. This is due to highly efficient, nontrivial search space traversal and pruning, and clause learning. One key component in driving search is the decision heuristics. Many different structure-based decision heuristics have been proposed, attempting to exploit knowledge of the underlying problem structure. In this talk I will present a high-level review of our work on analyzing the inherent limitations of structure-based decision heuristics. The main results are proof complexity theoretic hierarchies of heuristics, with exponential differences in the power of different heuristics.
Practical implications of such heuristics have also been considered through an extensive experimental evaluation.
Bio:
Dr. Matti Järvisalo received his doctorate in computer science from Helsinki University of Technology TKK in 2008, focusing on Boolean constraint reasoning. After the doctorate, Järvisalo has been a postdoctoral researcher in the Computational Logic Group at TKK and a visiting researcher in the Institute for Formal Models and Verification at Johannes Kepler University Linz, Austria. Currently he holds the position of Postdoctoral Researcher in the Department of Computer Science at University of Helsinki, and is a grantee of an Academy of Finland postdoctoral project starting from 2010. Järvisalo's main research interests include both theoretical and practical aspects of computationally hard constraint satisfaction and optimization problems, with an emphasis on efficient approaches for real-world applications.
Last updated on 5 Oct 2009 by Visa Noronen - Page created on 9 Oct 2009 by Visa Noronen