KTH / CSC / Theory Group / Jakob Nordström / Research project in proof complexity

Proof Complexity and SAT Solving

Principal Investigator

Jakob Nordström

Researchers

• Massimo Lauria, postdoctoral researcher.
• Mladen Mikša, PhD student.
• Marc Vinyals, PhD student.

Long-Term Visitors

(Visitors for one month or more.)

• Yuval Filmus, University of Toronto, November-December 2012
• Bangsheng Tang, Tsinghua University, January-February 2012
• Chris Beck, Princeton University, January-February 2012
• Trinh Huynh, University of Washington and ETH Zurich, August-September 2011

Short-Term Visitors

• Christoph Berkholz, RWTH Aachen University, April 2013
• Dominik Scheder, Aarhus University, February 2013
• Nicola Galesi and Ilario Bonacina, Sapienza University of Rome, February 2013
• Alexander Dreyer and Thanh Hung Nguyen, Fraunhofer Institute for Industrial Mathematics ITWM, November 2012
• Troy Lee, Centre for Quantum Technologies, October 2012
• Joshua Brody, Aarhus University, September 2012
• Rustan Leino, Microsoft Research Redmond, March 2012.
• Matti Järvisalo, University of Helsinki, December 2011
• Noga Ron-Zewi, Technion – Israel Institute of Technology, December 2011
• Arkadev Chattopadhyay, University of Toronto, September 2011
• Rahul Santhanam, University of Edinburgh, September 2011
• Arie Matsliah, IBM Research Haifa and Technion – Israel Institute of Technology, August 2011
• Stanislav Živný , University of Oxford, May 2011
• Iddo Tzameret, Tsinghua University, May 2011

Brief Description of Project

The text below is a somewhat quick-and-dirty description which will be updated and polished at some later point. Please feel free to contact Jakob Nordström if you would like to get more details.

Proving formulas in propositional logic is a problem of immense importance both theoretically and practically. On the one hand, this computational task is believed to be intractable in general, and deciding whether this is so is one of the famous million dollar Millennium Problems (the P vs. NP problem). On the other hand, today so-called SAT solvers are routinely used to solve large-scale real-world problem instances with millions of variables (while there are also small formulas known with just a couple of hundreds of variables that cause even state-of-the-art SAT solvers to stumble).

Proof complexity studies formal systems for reasoning about logic formulas. This field has deep connections to fundamental questions in computational complexity, but another important motivation is the connection to SAT solving. All SAT solvers explicitly or implicitly define a system in which proofs are searched for, and proof complexity can be seen to analyse the potential and limitations of such proof systems (and thereby of the algorithms using them).

In this project, we aim to advance the frontiers of proof complexity, and also hope to leverage this research to shed light on questions related to SAT solving. In one direction, we are interested in understanding what makes formulas hard or easy in practice by combining theoretical study and practical experiments, and also in gaining theoretical insights into other crucial but poorly understood issues in SAT solving. Another intriguing direction is to explore the possibility of basing SAT solvers on stronger proof systems than are currently being used. In order to do so, however, a crucial first step, and the main direction of the project, is to obtain a better understanding of candidate proof systems such as polynomial calculus and cutting planes. In this context there are a number of well-known open questions in proof complexity that we want to attack and solve, such as proving lower bounds on proof size and proof space as well as time-space trade-offs. Also, making progress on any other longstanding open questions in proof complexity is always of interest. Finally, it should be mentioned that proof complexity has turned out to have deep, and sometimes surprising, connections to other areas in theoretical computer science such as, for example, circuit complexity, communication complexity, and hardness of approximation. Therefore, the project could potentially also involve research in these or other related areas.

An overview of some of the problems of interest in this context, as well as of the state of the art regarding these problems, can be found in the survey Pebble Games, Proof Complexity, and Time-Space Trade-offs.

Funding

This project is funded by a Starting Independent Researcher Grant from the European Research Council as well as by a Junior Researcher Position Grant and a Breakthrough Research Grant from the Swedish Research Council.

Publications

A list of publications will be provided at some later point, but for now see this list of papers which should cover everything relevant.