Proof Complexity and SAT Solving
(Visitors for one month or more.)
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.
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.
A list of publications will be provided at some later point, but for now see this list of papers which should cover everything relevant.