Research Project on Proof Complexity and SAT Solving
Principal Investigator
Jakob Nordström
Researchers
LongTerm Visitors
(Visitors for one month or more.)

Ilario Bonacina,
Sapienza – Università di Roma,
JanuaryMay 2014

Navid Talebanfard,
Aarhus University, JanuaryMarch 2014

Yuval Filmus,
University of Toronto,
NovemberDecember 2012

Bangsheng Tang,
Tsinghua University,
JanuaryFebruary 2012

Chris Beck,
Princeton University,
JanuaryFebruary 2012

Trinh Huynh,
University of Washington and ETH Zurich,
AugustSeptember 2011
ShortTerm Visitors

Benjamin Rossman,
Tokyo Institute of Technology,
June 2014 (planned)

Prahladh Harsha,
Tata Institute of Fundamental Research, Mumbai,
March 2014

Jan Johannsen,
LudwigMaximiliansUniversität München,
March 2014

Siu Man Chan,
Princeton University,
December 2013

Daniel Le Berre,
Université d'Artois,
November 2013

Klas Markström,
Umeå University,
November 2013

Albert Atserias,
Universitat Politècnica de Catalunya,
August 2013

Christoph Berkholz,
RWTH Aachen University,
April 2013

Dominik Scheder,
Aarhus University,
February 2013

Nicola Galesi
and
Ilario Bonacina,
Sapienza – Università di Roma,
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 RonZewi,
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 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 socalled SAT solvers are routinely and
successfully used to solve largescale realworld 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 1015 years, there have been dramatic — and
surprising — developments in SAT solving technology that have
improved realworld 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 socalled
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
wellunderstood 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 wellknown
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
timespace tradeoffs. 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 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.
2014

Mladen Mikša and Jakob Nordström.
Long Proofs of (Seemingly) Simple Formulas.
Manuscript in submission, 2014.

Albert Atserias, Massimo Lauria, and Jakob Nordström.
Narrow Proofs May Be Maximally Long.
To appear in
Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC '14),
June 2014.

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 300311, March 2014.
2013

Jakob Nordström.
Pebble Games, Proof Complexity, and TimeSpace Tradeoffs.
Logical Methods in Computer Science,
volume 9, issue 3, article 15, September 2013.

Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A Characterization
of TreeLike Resolution Size. In Information Processing Letters,
volume 113, number 18,
pages 666671, September 2013.

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.

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 351364, July 2013.

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 437448, July 2013.

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 684695, July 2013.

Chris Beck, Jakob Nordström, and Bansheng Tang.
Some Tradeoff Results for Polynomial Calculus (Extended Abstract).
In
Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13),
pages 813822,
June 2013.

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 471557, May 2013.
2012

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga RonZewi, and Neil Thapen.
Space Complexity in Polynomial Calculus.
Technical Report TR12132,
Electronic Colloquium on Computational Complexity (ECCC),
October 2012.

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 316331, October 2012.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A.
Razborov. Parameterized Boundeddepth Frege Is Not Optimal. In
ACM Transaction on Computational Theory,
volume 4, issue 3, article 7,
September 2012.

Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga RonZewi.
Space Complexity in Polynomial Calculus (Extended Abstract).
In
Proceedings of the 27th Annual IEEE Conference on Computational Complexity (CCC '12),
pages 334344, June 2012.

Trinh Huynh and Jakob Nordström.
On the Virtue of Succinct Proofs:
Amplifying Communication Complexity Hardness to
TimeSpace Tradeoffs in Proof Complexity (Extended Abstract).
In
Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC '12),
pages 233248, May 2012.

Jakob Nordström.
On the Relative Strength of Pebbling and Resolution.
ACM Transactions on Computational Logic,
volume 13, issue 2, article 16, April 2012.
2011

Jakob Nordström and Alexander Razborov.
On Minimal Unsatisfiability and
TimeSpace Tradeoffs for kDNF Resolution.
In
Proceedings of the 38th International Colloquium on
Automata, Languages and Programming (ICALP '11),
Lecture Notes in Computer Science, volume 6755,
pages 642653, July 2011.

Eli BenSasson and Jakob Nordström.
Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions (Extended Abstract).
In
Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11),
pages 401416, January 2011.
