swe flag På svenska
bild
School of
Computer Science
and Communication
KTH / CSC / Theory Group / Jakob Nordström / Research project on proof complexity and SAT solving

Research Project on Proof Complexity and SAT Solving

Principal Investigator

Jakob Nordström

Researchers

  • Massimo Lauria, postdoctoral researcher (since 2012).
  • Jan Elffers, PhD student (starting September 2014).
  • Mladen Mikša, PhD student (since 2012).
  • Susanna Figueiredo de Rezende, PhD student (starting August 2014).
  • Marc Vinyals, PhD student (since 2012).

Long-Term Visitors

(Visitors for one month or more.)

  • Ilario Bonacina, Sapienza – Università di Roma, January-May 2014
  • Navid Talebanfard, Aarhus University, January-March 2014
  • 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

Brief Description of Project

The purpose of this research project is to explore one of the most significant problems in all of computer science, namely that of proving logic formulas. This 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 and successfully used to solve large-scale real-world formulas in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and railway signalling systems, just to name a few examples).

During the last 10-15 years, there have been dramatic — and surprising — developments in SAT solving technology that have improved real-world performance by many orders of magnitude. But perhaps even more surprisingly, the best SAT solvers today are still based on relatively simple methods from the early 1960s (albeit with many clever optimizations), searching for proofs in the so-called resolution proof system. While such solvers can often handle formulas with millions of variables, there are also known tiny formulas with just a few hundred variables that cause even the very best solvers to stumble. The fundamental questions of when SAT solvers perform well or badly, and what properties of the formulas influence SAT solver performance, remain very poorly understood. Other practical SAT solving issues, such as how to optimize memory management and how to exploit parallelization on modern multicore architectures, are even less well studied and understood from a theoretical point of view.

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). During the last couple of decades other mathematical methods of reasoning than resolution have been studied and have been shown to be much stronger than resolution, in particular methods based on algebra and geometry. It is an intriguing fact, however, that so far attempts to harness the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. And while resolution is a reasonably well-understood proof system, even very basic questions about these stronger algebraic and geometric methods remain wide open.

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, e.g., 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.

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.

Workshops

Workshops, seminar weeks, et cetera (co-)organized by Jakob Nordström in connection with this project:

Publications

Below follows a list of publications, sorted in reverse chronological order, resulting from this project. As a general rule, these papers are copyright by their respective publishers but are free for personal use.

See www.csc.kth.se/~jakobn/research/ for a full list of Jakob Nordströ'ms publications.

2014

  • Mladen Mikša and Jakob Nordström. Long Proofs of (Seemingly) Simple Formulas. To appear in Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT '14), July 2014. PDF
  • Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow Proofs May Be Maximally Long (Extended Abstract). In Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC '14), pages 286-297, June 2014. PDF
  • Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. From Small Space to Small Width in Resolution. In Proceedings of the 31st Symposium on Theoretical Aspects of Computer Science (STACS '14), pages 300-311, March 2014. PDF

2013

  • Jakob Nordström. Pebble Games, Proof Complexity, and Time-Space Trade-offs. Logical Methods in Computer Science, volume 9, issue 3, article 15, September 2013. PDF
  • Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A Characterization of Tree-Like Resolution Size. In Information Processing Letters, volume 113, number 18, pages 666-671, September 2013. PDF
  • Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Parameterized Complexity of DPLL Search Procedures In ACM Transactions on Computational Logic, volume 14, issue 3, article 23, August 2013. PDF
  • Massimo Lauria. A Rank Lower Bound for Cutting Planes Proofs of Ramsey Theorem. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13), pages 351-364, July 2013. PDF
  • Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds (Extended Abstract). In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP '13), Lecture Notes in Computer Science, volume 7965, pages 437-448, July 2013. PDF
  • Massimo Lauria, Pavel Pudlak, Vojtěch Rödl, and Neil Thapen. The Complexity of Proving That a Graph Is Ramsey. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP '13), Lecture Notes in Computer Science, volume 7965, pages 684-695, July 2013. PDF
  • Chris Beck, Jakob Nordström, and Bansheng Tang. Some Trade-off Results for Polynomial Calculus (Extended Abstract). In Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13), pages 813-822, June 2013. PDF
  • Jakob Nordström and Johan Håstad. Towards an Optimal Separation of Space and Length in Resolution. Theory of Computing, volume 9, article 14, pages 471-557, May 2013. PDF

2012

  • Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. Space Complexity in Polynomial Calculus. Technical Report TR12-132, Electronic Colloquium on Computational Complexity (ECCC), October 2012. PDF
  • Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný. Relating Proof Complexity Measures and Practical Hardness of SAT. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP '12), pages 316-331, October 2012. PDF
  • Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A. Razborov. Parameterized Bounded-depth Frege Is Not Optimal. In ACM Transaction on Computational Theory, volume 4, issue 3, article 7, September 2012. PDF
  • Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga Ron-Zewi. Space Complexity in Polynomial Calculus (Extended Abstract). In Proceedings of the 27th Annual IEEE Conference on Computational Complexity (CCC '12), pages 334-344, June 2012. PDF
  • Trinh Huynh and Jakob Nordström. On the Virtue of Succinct Proofs: Amplifying Communication Complexity Hardness to Time-Space Trade-offs in Proof Complexity (Extended Abstract). In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC '12), pages 233-248, May 2012. PDF
  • Jakob Nordström. On the Relative Strength of Pebbling and Resolution. ACM Transactions on Computational Logic, volume 13, issue 2, article 16, April 2012. PDF

2011

  • Jakob Nordström and Alexander Razborov. On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution. In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP '11), Lecture Notes in Computer Science, volume 6755, pages 642-653, July 2011. PDF
  • Eli Ben-Sasson and Jakob Nordström. Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions (Extended Abstract). In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11), pages 401-416, January 2011. PDF
Published by: Jakob Nordström <jakobn~at-sign~kth~dot~se>
Updated 2014-07-05