 |
Computable Short Proofs
Marijn J.H. Heule, University of Texas at Austin, US |
| Abstract: The success of satisfiability solving presents us with an interesting peculiarity: modern solvers can frequently handle gigantic formulas while failing miserably on supposedly easy problems. Their poor performance is typically caused by the weakness of their underlying proof system—resolution. To overcome this obstacle, we need solvers that are based on stronger proof systems. Unfortunately, existing strong proof systems—such as extended resolution or Frege systems—do not seem to lend themselves to mechanization. We present a new proof system that not only generalizes strong existing proof systems but that is also well-suited for mechanization. The proof system is surprisingly strong, even without the introduction of new variables—a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of the new proof system on the famous pigeon hole formulas by providing short proofs without new variables. Moreover, we introduce satisfaction-driven clause learning, a new decision procedure that exploits the strengths of our new proof system and can therefore yield exponential speed-ups compared to state-of-the-art solvers based on resolution. |
|
| Bio: Marijn Heule is a Research Assistant Professor at the University of Texas at Austin and received his PhD at Delft University of Technology (2008). His contributions to SAT solving have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning SAT solvers and his preprocessing and proof producing techniques are used in many state-of-the-art solvers. | |
|
Modelling SAT
Rahul Santhanam, University of Oxford, UK |
 |
| Abstract: SAT is a fundamental computational problem and there are several approaches to modelling its complexity: exact algorithms, proof complexity and random constraint satisfaction. I will briefly survey these approaches, and point out their respective strengths and weaknesses. I will identify certain questions that do not seem to be answerable within any individual approach. This suggests the need for a more inter-disciplinary perspective – I will mention some promising results in this direction. |
|
| Bio: Rahul Santhanam is Professor of Computing Science at Oxford. He completed his PhD at the University of Chicago in 2005. After postdocs at Simon Fraser University and the University of Toronto, he was first Lecturer and then Reader in the School of Informatics at the University of Edinburgh. He moved to his present post in 2016. His main research interests are in computational complexity, proof complexity and exact algorithms for Satisfiability and other NP-complete problems. | |
 |
Dependency Quantified Boolean Formulas: An
Overview of Solution Methods and Applications Christoph Scholl, Albert-Ludwigs-University Freiburg, DE |
| Abstract: Dependency quantified Boolean formulas (DQBFs) as a generalization of quantified Boolean formulas (QBFs) have received considerable attention in research during the last years. Here we give an overview of the solution methods developed for DQBF so far. The exposition is complemented with the discussion of various applications that can be handled with DQBF solving. | |
| Bio: Christoph Scholl received the Dipl.-Inform. and the Dr.-Ing. degrees in Computer Science from University of Saarland, Germany, in 1993 and 1997, respectively. In 2002 he received the venia legendi from University of Freiburg, Germany. In 2002/2003 he was an associate professor for computer engineering at the University of Heidelberg and in 2003 he joined the University of Freiburg as a professor in the Department of Computer Science. His research interests include logic synthesis, real-time operating systems, and the verification both of digital circuits and systems and of timed and hybrid systems. In this context a main focus of his work lies on the development of efficient symbolic data structures and algorithms as well as new solver techniques. | |