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 15-20 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 has been funded by a Starting Independent Researcher Grant
from the European Research Council
as well as by a
Junior Researcher Position Grant,
a
Breakthrough Research Grant,
and a Consolidator Grant
from the Swedish Research Council.
Workshops
Workshops, seminar weeks, et cetera co-organized by Jakob Nordström
in connection with this project:
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.
Please note that the list below is updated at somewhat irregular intervals
and is currently seriously out-of-date.
See
www.csc.kth.se/~jakobn/research/
for a full list of Jakob Nordström's publications
(which is updated much more frequently, but does not contain papers by other
members of the group on which Jakob Nordström is not a co-author).
2018
Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov.
Adventures in Monotone Complexity and TFNP.
Technical Report TR18-163,
Electronic Colloquium on Computational Complexity (ECCC),
September 2018.
Jan Elffers and Jakob Nordström.
Divide and Conquer: Towards Faster Pseudo-Boolean Solving.
In
Proceedings of the 27th International Joint Conference on
Artificial Intelligence (IJCAI '18),
pages 1291-1299, July 2018.
Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, and
Laurent Simon.
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks.
In
Proceedings of the 27th International Joint Conference on
Artificial Intelligence (IJCAI '18),
pages 1300-1308, July 2018.
Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, and Marc Vinyals.
Using Combinatorial Benchmarks to Probe the Reasoning Power of
Pseudo-Boolean Solvers.
In
Proceedings of the 21st International Conference on
Theory and Applications of Satisfiability Testing (SAT '18),
Lecture Notes in Computer Science, volume 10929,
pages 75-93, July 2018.
Marc Vinyals, Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and Jakob Nordström.
In Between Resolution and Cutting Planes: A Study of Proof Systems
for Pseudo-Boolean SAT Solving.
In
Proceedings of the 21st International Conference on
Theory and Applications of Satisfiability Testing (SAT '18),
Lecture Notes in Computer Science, volume 10929,
pages 292-310, July 2018.
Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria,
Jakob Nordström, and Alexander Razborov.
Clique Is Hard on Average for Regular Resolution.
In
Proceedings of the 50th Annual ACM Symposium on Theory of Computing
(STOC '18),
pages 866-877, June 2018.
Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov.
Monotone circuit lower bounds from resolution.
In
Proceedings of the 50th Annual ACM Symposium on Theory of Computing
(STOC '18),
pages 902-911, June 2018.
Arkadev Chattopadhyay, Michal Koucký, Bruno Loff, and Sagnik Mukhopadhyay.
Simulation Beats Richness: New Data-Structure Lower Bounds.
In
Proceedings of the 50th Annual ACM Symposium on Theory of Computing
(STOC '18),
pages 1013-1020, June 2018.
Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov.
Reordering Rule Makes OBDD Proof Systems Stronger.
In
Proceedings of the 33rd Annual Computational Complexity Conference
(CCC '17),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 102, pages 16:1-16:24, June 2018.
2017
Ilario Bonacina.
Space in Weak Propositional Proof Systems.
Springer, 2017.
Massimo Lauria and Jakob Nordström.
Tight Size-Degree Bounds for Sums-of-Squares Proofs.Computational Complexity,
volume 26, issue 3, pages 911-948, December 2017.
Ilario Bonacina and Navid Talebanfard.
Strong ETH and Resolution via Games and the Multiplicity of Strategies.Algorithmica,
volume 79, issue 1, pages 29-41, September 2017.
Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, and Jordi Levy.
Structure Features for SAT Instances ClassificationJournal of Applied Logic,
volume 23, pages 27-39, September 2017.
Jesús Giráldez-Cru and Jordi Levy.
Locality in Random SAT Instances.
In
Proceedings of the 26th International Joint Conference on
Artificial Intelligence (IJCAI '17),
pages 638-644, August 2017.
Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals.
CNFgen: A Generator of Crafted Benchmarks.
In
Proceedings of the 20th International Conference on
Theory and Applications of Satisfiability Testing (SAT '17),
Lecture Notes in Computer Science, volume 10491,
pages 464-473, August 2017.
Guillaume Baud-Berthier, Jesús Giráldez-Cru, and Laurent Simon.
On the Community Structure of Bounded Model Checking SAT Problems.
In
Proceedings of the 20th International Conference on
Theory and Applications of Satisfiability Testing (SAT '17),
Lecture Notes in Computer Science, volume 10491,
pages 65-82, August 2017.
Patrick Bennett, Ilario Bonacina, Nicola Galesi,
Tony Huynh, Mike Molloy, and Paul Wollan.
Space proof complexity for random 3-CNFs.Information and Computation,
volume 255, part 1, pages 165-176, August 2017.
Massimo Lauria and Jakob Nordström.
Graph Colouring is Hard for Algorithms Based on
Hilbert's Nullstellensatz and Gröbner Bases.
In
Proceedings of the 32nd Annual Computational Complexity Conference (CCC '17),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 79, pages 2:1-2:20,
July 2017.
Massimo Lauria, Pavel Pudlák,
Vojtěch Rödl and Neil Thapen.
The Complexity of Proving That a Graph Is Ramsey.Combinatorica,
volume 37, issue 2, pages 253-268,
April 2017.
Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals.
Cumulative Space in Black-White Pebbling and Resolution.
In
Proceedings of the 8th Innovations in
Theoretical Computer Science Conference (ITCS '17),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 67, pages 38:1-38:21,
January 2017.
2016
Christoph Berkholz and Jakob Nordström.
Supercritical Space-Width Trade-offs for Resolution.
Technical Report TR16-203,
Electronic Colloquium on Computational Complexity (ECCC),
December 2016.
Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals.
How Limited Interaction Hinders Real Communication
(and What It Means for Proof and Circuit Complexity).
In
Proceedings of the 57th Annual IEEE Symposium on
Foundations of Computer Science (FOCS '16),
pages 295-304, October 2016.
Ilario Bonacina, Nicola Galesi, and Neil Thapen.
Total Space in Resolution.SIAM Journal on Computing,
volume 45, issue 5, pages 1894-1909, October 2016.
Christoph Berkholz and Jakob Nordström.
Near-Optimal Lower Bounds on Quantifier Depth and
Weisfeiler-Leman Refinement Steps.
Technical Report TR16-135,
Electronic Colloquium on Computational Complexity (ECCC),
August 2016.
Christoph Berkholz and Jakob Nordström.
Supercritical Space-Width Trade-offs for Resolution.
In
Proceedings of the 43rd International Colloquium on
Automata, Languages and Programming (ICALP '16),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 55, pages 57:1-57:14, July 2016.
Ilario Bonacina.
Total Space in Resolution Is at Least Width Squared.
In
Proceedings of the 43rd International Colloquium on
Automata, Languages and Programming (ICALP '16),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 55, pages 56:1-56:13, July 2016.
Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard,
Jakob Nordström, and Marc Vinyals.
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers.
In
Proceedings of the 19th International Conference on
Theory and Applications of Satisfiability Testing (SAT '16),
Lecture Notes in Computer Science, volume 9710,
pages 160-176, July 2016.
Christoph Berkholz and Jakob Nordström.
Near-Optimal Lower Bounds on Quantifier Depth and
Weisfeiler-Leman Refinement Steps.
In
Proceedings of the 31st Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS '16),
July 2016.
Massimo Lauria.
A Rank Lower Bound for Cutting Planes Proofs of
Ramsey's Theorem.ACM Transactions on Computation Theory,
volume 8, issue 4, article 17, June 2016.
Albert Atserias, Massimo Lauria, and Jakob Nordström.
Narrow Proofs May Be Maximally Long.
In
ACM Transactions on Computational Logic,
volume 17, issue 3, article 19, May 2016.
Yuval Filmus, Pavel Hrubeš, and Massimo Lauria.
Semantic Versus Syntactic Cutting Planes.
In
Proceedings of the 33rd Symposium on Theoretical Aspects of
Computer Science (STACS '16),
pages 35:1-35:13, February 2016.
Ilario Bonacina and Navid Talebanfard.
Improving Resolution Width Lower Bounds for k-CNFs with Applications to the
Strong Exponential Time Hypothesis.Information Processing Letters,
volume 116, issue 2, pages 120-124, February 2016.
Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew.
Lower Bounds: From Circuits to QBF Proof Systems.
In
Proceedings of the 7th Innovations in
Theoretical Computer Science Conference (ITCS '16),
pages 249-260, January 2016.
2015
Siu Man Chan, Massimo Lauria, Jakob Nordström, and Marc Vinyals.
Hardness of Approximation in PSPACE and Separation
Results for Pebble Games (Extended Abstract).
In
Proceedings of the 56th Annual IEEE Symposium on
Foundations of Computer Science (FOCS '15),
pages 466-485,
October 2015.
Ilario Bonacina and Navid Talebanfard.
Strong ETH and Resolution via Games and the Multiplicity of Strategies.
In
Proceedings of the 10th International Symposium on Parameterized and
Exact Computation (IPEC '15),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 43, pages 248-257, September 2015.
Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen.
Space Complexity in Polynomial Calculus.SIAM Journal on Computing,
volume 44, issue 4, pages 1119-1153, August 2015.
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals.
From Small Space to Small Width in Resolution.ACM Transactions on Computational Logic,
volume 16, issue 4, article 28, July 2015.
Jakob Nordström.
On the Interplay Between Proof Complexity and SAT Solving.ACM SIGLOG News,
volume 2, number 3, pages 19-44, July 2015.
(Lightly edited version with some typos fixed.)
Massimo Lauria and Jakob Nordström.
Tight Size-Degree Bounds for Sums-of-Squares Proofs.
In
Proceedings of the 30th Annual
Computational Complexity Conference (CCC '15),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 33, pages 448-466,
June 2015.
Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
In
Proceedings of the 30th Annual
Computational Complexity Conference (CCC '15),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 33, pages 467-487,
June 2015.
Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
Technical Report TR15-078,
Electronic Colloquium on Computational Complexity (ECCC),
May 2015.
Massimo Lauria and Jakob Nordström.
Tight Size-Degree Bounds for
Sums-of-Squares Proofs.
Technical Report TR15-053,
Electronic Colloquium on Computational Complexity (ECCC),
April 2015.
2014
Jakob Nordström.
A (Biased) Proof Complexity Survey for SAT Practitioners.
In
Proceedings of the 17th International Conference on
Theory and Applications of Satisfiability Testing (SAT '14),
Lecture Notes in Computer Science, volume 8561,
pages 1-6, July 2014.
Mladen Mikša and Jakob Nordström.
Long Proofs of (Seemingly) Simple Formulas.
In
Proceedings of the 17th International Conference on
Theory and Applications of Satisfiability Testing (SAT '14),
Lecture Notes in Computer Science, volume 8561,
pages 121-137, July 2014.
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.
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.
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.
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.
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 351-364, 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 437-448, 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 684-695, July 2013.
Chris Beck, Jakob Nordström, and Bangsheng 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.
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.
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.
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.
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.
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.
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.
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
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.
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.
På svenska
