Search Results

Documents authored by Nordström, Jakob

Document
DOI: 10.4230/LIPIcs.CP.2024.4
Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

Authors: Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.
Cite as

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berg_et_al:LIPIcs.CP.2024.4,
  author =	{Berg, Jeremias and Bogaerts, Bart and Nordstr\"{o}m, Jakob and Oertel, Andy and Paxian, Tobias and Vandesande, Dieter},
  title =	{{Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{4:1--4:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.4},
  URN =		{urn:nbn:de:0030-drops-206895},
  doi =		{10.4230/LIPIcs.CP.2024.4},
  annote =	{Keywords: proof logging, certifying algorithms, MaxSAT, solution-improving search, SAT-UNSAT, maximum satisfiability, combinatorial optimization, certification, pseudo-Boolean}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.9
Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms

Authors: Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic programming based knapsack propagator inside a constraint programming solver.
Cite as

Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov. Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{demirovic_et_al:LIPIcs.CP.2024.9,
  author =	{Demirovi\'{c}, Emir and McCreesh, Ciaran and McIlree, Matthew J. and Nordstr\"{o}m, Jakob and Oertel, Andy and Sidorov, Konstantin},
  title =	{{Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.9},
  URN =		{urn:nbn:de:0030-drops-206948},
  doi =		{10.4230/LIPIcs.CP.2024.9},
  annote =	{Keywords: Proof logging, dynamic programming, decision diagrams}
}
Document
DOI: 10.4230/LIPIcs.CP.2023.27
Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning

Authors: Gioni Mexi, Timo Berthold, Ambros Gleixner, and Jakob Nordström

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
Conflict analysis has been successfully generalized from Boolean satisfiability (SAT) solving to mixed integer programming (MIP) solvers, but although MIP solvers operate with general linear inequalities, the conflict analysis in MIP has been limited to reasoning with the more restricted class of clausal constraint. This is in contrast to how conflict analysis is performed in so-called pseudo-Boolean solving, where solvers can reason directly with 0-1 integer linear inequalities rather than with clausal constraints extracted from such inequalities. In this work, we investigate how pseudo-Boolean conflict analysis can be integrated in MIP solving, focusing on 0-1 integer linear programs (0-1 ILPs). Phrased in MIP terminology, conflict analysis can be understood as a sequence of linear combinations and cuts. We leverage this perspective to design a new conflict analysis algorithm based on mixed integer rounding (MIR) cuts, which theoretically dominates the state-of-the-art division-based method in pseudo-Boolean solving. We also report results from a first proof-of-concept implementation of different pseudo-Boolean conflict analysis methods in the open-source MIP solver SCIP. When evaluated on a large and diverse set of 0-1 ILP instances from MIPLIB2017, our new MIR-based conflict analysis outperforms both previous pseudo-Boolean methods and the clause-based method used in MIP. Our conclusion is that pseudo-Boolean conflict analysis in MIP is a promising research direction that merits further study, and that it might also make sense to investigate the use of such conflict analysis to generate stronger no-goods in constraint programming.
Cite as

Gioni Mexi, Timo Berthold, Ambros Gleixner, and Jakob Nordström. Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mexi_et_al:LIPIcs.CP.2023.27,
  author =	{Mexi, Gioni and Berthold, Timo and Gleixner, Ambros and Nordstr\"{o}m, Jakob},
  title =	{{Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{27:1--27:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.27},
  URN =		{urn:nbn:de:0030-drops-190641},
  doi =		{10.4230/LIPIcs.CP.2023.27},
  annote =	{Keywords: Integer programming, pseudo-Boolean solving, conflict analysis, cutting planes proof system, mixed integer rounding, division, saturation}
}
Document
DOI: 10.4230/DagRep.12.10.84
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)

Authors: Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel

Published in: Dagstuhl Reports, Volume 12, Issue 10 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22411 "Theory and Practice of SAT and Combinatorial Solving". The purpose of this workshop was to explore the Boolean satisfiability (SAT) problem, which plays a fascinating dual role in computer science. By the theory of NP-completeness, this problem captures thousands of important applications in different fields, and a rich mathematical theory has been developed showing that all these problems are likely to be infeasible to solve in the worst case. But real-world problems are typically not worst-case, and in recent decades exceedingly efficient algorithms based on so-called conflict-driven clause learning (CDCL) have turned SAT solvers into highly practical tools for solving large-scale real-world problems in a wide range of application areas. Analogous developments have taken place for problems beyond NP such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, satisfiability modulo theories (SMT) solving, quantified Boolean formula (QBF) solving, constraint programming, and mixed integer programming, where the conflict-driven paradigm has sometimes been added to other powerful techniques. The current state of the art in combinatorial solving presents a host of exciting challenges at the borderline between theory and practice. Can we gain a deeper scientific understanding of the techniques and heuristics used in modern combinatorial solvers and why they are so successful? Can we develop tools for rigorous analysis of the potential and limitations of these algorithms? Can computational complexity theory be extended to shed light on real-world settings that go beyond worst case? Can more powerful methods of reasoning developed in theoretical research be harnessed to yield improvements in practical performance? And can state-of-the-art combinatorial solvers be enhanced to not only solve problems, but also provide verifiable proofs of correctness for the solutions they produce? This workshop gathered leading applied and theoretical researchers working on SAT and combinatorial optimization more broadly in order to stimulate an exchange of ideas and techniques. We see great opportunities for fruitful interplay between theory and practice in these areas, as well as for technology transfer between different paradigms in combinatorial optimization, and our assessment is that this workshop demonstrated very convincingly that a more vigorous interaction has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel. Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). In Dagstuhl Reports, Volume 12, Issue 10, pp. 84-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.12.10.84,
  author =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  title =	{{Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)}},
  pages =	{84--105},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.10.84},
  URN =		{urn:nbn:de:0030-drops-178212},
  doi =		{10.4230/DagRep.12.10.84},
  annote =	{Keywords: Boolean satisfiability (SAT), SAT solving, computational complexity, proof complexity, combinatorial solving, combinatorial optimization, constraint programming, mixed integer linear programming}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.16
Certified CNF Translations for Pseudo-Boolean Solving

Authors: Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.
Cite as

Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gocht_et_al:LIPIcs.SAT.2022.16,
  author =	{Gocht, Stephan and Martins, Ruben and Nordstr\"{o}m, Jakob and Oertel, Andy},
  title =	{{Certified CNF Translations for Pseudo-Boolean Solving}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{16:1--16:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.16},
  URN =		{urn:nbn:de:0030-drops-166901},
  doi =		{10.4230/LIPIcs.SAT.2022.16},
  annote =	{Keywords: pseudo-Boolean solving, 0-1 integer linear program, proof logging, certifying algorithms, certified translation, CNF encoding, cutting planes}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.25
An Auditable Constraint Programming Solver

Authors: Stephan Gocht, Ciaran McCreesh, and Jakob Nordström

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
We describe the design and implementation of a new constraint programming solver that can produce an auditable record of what problem was solved and how the solution was reached. As well as a solution, this solver provides an independently verifiable proof log demonstrating that the solution is correct. This proof log uses the VeriPB proof system, which is based upon cutting planes reasoning with extension variables. We explain how this system can support global constraints, variables with large domains, and reformulation, despite not natively understanding any of these concepts.
Cite as

Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An Auditable Constraint Programming Solver. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gocht_et_al:LIPIcs.CP.2022.25,
  author =	{Gocht, Stephan and McCreesh, Ciaran and Nordstr\"{o}m, Jakob},
  title =	{{An Auditable Constraint Programming Solver}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.25},
  URN =		{urn:nbn:de:0030-drops-166548},
  doi =		{10.4230/LIPIcs.CP.2022.25},
  annote =	{Keywords: Constraint programming, proof logging, auditable solving}
}
Document
DOI: 10.4230/LIPIcs.CCC.2021.40
The Power of Negative Reasoning

Authors: Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

Abstract
Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.
Cite as

Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The Power of Negative Reasoning. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{derezende_et_al:LIPIcs.CCC.2021.40,
  author =	{de Rezende, Susanna F. and Lauria, Massimo and Nordstr\"{o}m, Jakob and Sokolov, Dmitry},
  title =	{{The Power of Negative Reasoning}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{40:1--40:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.40},
  URN =		{urn:nbn:de:0030-drops-143140},
  doi =		{10.4230/LIPIcs.CCC.2021.40},
  annote =	{Keywords: Proof complexity, Polynomial calculus, Nullstellensatz, Sums-of-squares, Sherali-Adams}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.28
Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs

Authors: Susanna F. de Rezende, Jakob Nordström, Kilian Risse, and Dmitry Sokolov

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. We obtain our results by revisiting Razborov’s pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.
Cite as

Susanna F. de Rezende, Jakob Nordström, Kilian Risse, and Dmitry Sokolov. Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 28:1-28:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{derezende_et_al:LIPIcs.CCC.2020.28,
  author =	{de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Risse, Kilian and Sokolov, Dmitry},
  title =	{{Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{28:1--28:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.28},
  URN =		{urn:nbn:de:0030-drops-125804},
  doi =		{10.4230/LIPIcs.CCC.2020.28},
  annote =	{Keywords: proof complexity, resolution, weak pigeonhole principle, perfect matching, sparse graphs}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.72
Trade-Offs Between Size and Degree in Polynomial Calculus

Authors: Guillaume Lagarde, Jakob Nordström, Dmitry Sokolov, and Joseph Swernofsky

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
Building on [Clegg et al. '96], [Impagliazzo et al. '99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(√(n log S)). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen '16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.
Cite as

Guillaume Lagarde, Jakob Nordström, Dmitry Sokolov, and Joseph Swernofsky. Trade-Offs Between Size and Degree in Polynomial Calculus. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lagarde_et_al:LIPIcs.ITCS.2020.72,
  author =	{Lagarde, Guillaume and Nordstr\"{o}m, Jakob and Sokolov, Dmitry and Swernofsky, Joseph},
  title =	{{Trade-Offs Between Size and Degree in Polynomial Calculus}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{72:1--72:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.72},
  URN =		{urn:nbn:de:0030-drops-117573},
  doi =		{10.4230/LIPIcs.ITCS.2020.72},
  annote =	{Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, size-degree trade-off, resolution, colored polynomial local search}
}
Document
DOI: 10.4230/LIPIcs.CCC.2019.18
Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling

Authors: Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)

Abstract
We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatz refutation of the pebbling formula over G in size t+1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.
Cite as

Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{derezende_et_al:LIPIcs.CCC.2019.18,
  author =	{de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Meir, Or and Robere, Robert},
  title =	{{Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.18},
  URN =		{urn:nbn:de:0030-drops-108403},
  doi =		{10.4230/LIPIcs.CCC.2019.18},
  annote =	{Keywords: proof complexity, Nullstellensatz, pebble games, trade-offs, size, degree}
}
Document
DOI: 10.4230/DagRep.8.1.124
Proof Complexity (Dagstuhl Seminar 18051)

Authors: Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam

Published in: Dagstuhl Reports, Volume 8, Issue 1 (2018)

Abstract
The study of proof complexity was initiated in [Cook and Reckhow 1979] as a way to attack the P vs.NP problem, and in the ensuing decades many powerful techniques have been discovered for analyzing different proof systems. Proof complexity also gives a way of studying subsystems of Peano Arithmetic where the power of mathematical reasoning is restricted, and to quantify how complex different mathematical theorems are measured in terms of the strength of the methods of reasoning required to establish their validity. Moreover, it allows to analyse the power and limitations of satisfiability algorithms (SAT solvers) used in industrial applications with formulas containing up to millions of variables. During the last 10--15 years the area of proof complexity has seen a revival with many exciting results, and new connections have also been revealed with other areas such as, e.g., cryptography, algebraic complexity theory, communication complexity, and combinatorial optimization. While many longstanding open problems from the 1980s and 1990s still remain unsolved, recent progress gives hope that the area may be ripe for decisive breakthroughs. This workshop, gathering researchers from different strands of the proof complexity community, gave opportunities to take stock of where we stand and discuss the way ahead.
Cite as

Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam. Proof Complexity (Dagstuhl Seminar 18051). In Dagstuhl Reports, Volume 8, Issue 1, pp. 124-157, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{atserias_et_al:DagRep.8.1.124,
  author =	{Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul},
  title =	{{Proof Complexity (Dagstuhl Seminar 18051)}},
  pages =	{124--157},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{1},
  editor =	{Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.1.124},
  URN =		{urn:nbn:de:0030-drops-92864},
  doi =		{10.4230/DagRep.8.1.124},
  annote =	{Keywords: bounded arithmetic, computational complexity, logic, proof complexity, satisfiability algorithms}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2017.38
Cumulative Space in Black-White Pebbling and Resolution

Authors: Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals

Published in: LIPIcs, Volume 67, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017)

Abstract
We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko 2015] as a tool for obtaining results in cryptography. We consider instead the nondeterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10-15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström 2008, 2011], we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.
Cite as

Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. Cumulative Space in Black-White Pebbling and Resolution. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{alwen_et_al:LIPIcs.ITCS.2017.38,
  author =	{Alwen, Jo\"{e}l and de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Vinyals, Marc},
  title =	{{Cumulative Space in Black-White Pebbling and Resolution}},
  booktitle =	{8th Innovations in Theoretical Computer Science Conference (ITCS 2017)},
  pages =	{38:1--38:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-029-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{67},
  editor =	{Papadimitriou, Christos H.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2017.38},
  URN =		{urn:nbn:de:0030-drops-81918},
  doi =		{10.4230/LIPIcs.ITCS.2017.38},
  annote =	{Keywords: pebble game, pebbling, proof complexity, space, cumulative space, clause space, resolution, parallel resolution}
}
Document
DOI: 10.4230/LIPIcs.CCC.2017.2
Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gröbner Bases

Authors: Massimo Lauria and Jakob Nordström

Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)

Abstract
We consider the graph k-colouring problem encoded as a set of polynomial equations in the standard way. We prove that there are bounded-degree graphs that do not have legal k-colourings but for which the polynomial calculus proof system defined in [Clegg et al. '96, Alekhnovich et al. '02] requires linear degree, and hence exponential size, to establish this fact. This implies a linear degree lower bound for any algorithms based on Gröbner bases solving graph k-colouring} using this encoding. The same bound applies also for the algorithm studied in a sequence of papers [De Loera et al. '08, '09, '11, '15] based on Hilbert's Nullstellensatz proofs for a slightly different encoding, thus resolving an open problem mentioned, e.g., in [De Loera et al. '09] and [Li et al. '16]. We obtain our results by combining the polynomial calculus degree lower bound for functional pigeonhole principle (FPHP) formulas over bounded-degree bipartite graphs in [Miksa and Nordström '15] with a reduction from FPHP to k-colouring derivable by polynomial calculus in constant degree.
Cite as

Massimo Lauria and Jakob Nordström. Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gröbner Bases. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{lauria_et_al:LIPIcs.CCC.2017.2,
  author =	{Lauria, Massimo and Nordstr\"{o}m, Jakob},
  title =	{{Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gr\"{o}bner Bases}},
  booktitle =	{32nd Computational Complexity Conference (CCC 2017)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-040-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{79},
  editor =	{O'Donnell, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.2},
  URN =		{urn:nbn:de:0030-drops-75410},
  doi =		{10.4230/LIPIcs.CCC.2017.2},
  annote =	{Keywords: proof complexity, Nullstellensatz, Gr\"{o}bner basis, polynomial calculus, cutting planes, colouring}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.57
Supercritical Space-Width Trade-Offs for Resolution

Authors: Christoph Berkholz and Jakob Nordström

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben-Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov’s new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].
Cite as

Christoph Berkholz and Jakob Nordström. Supercritical Space-Width Trade-Offs for Resolution. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 57:1-57:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICALP.2016.57,
  author =	{Berkholz, Christoph and Nordstr\"{o}m, Jakob},
  title =	{{Supercritical Space-Width Trade-Offs for Resolution}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{57:1--57:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.57},
  URN =		{urn:nbn:de:0030-drops-62266},
  doi =		{10.4230/LIPIcs.ICALP.2016.57},
  annote =	{Keywords: Proof complexity, resolution, space, width, trade-offs, supercritical}
}
Document
DOI: 10.4230/DagRep.5.4.98
Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)

Authors: Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15171 "Theory and Practice of SAT Solving". The purpose of this workshop was to explore one of the most significant problems in all of computer science, namely that of computing whether formulas in propositional logic are satisfiable or not. This problem is believed to be intractable in general (by the theory of NP-completeness). However, the last two decades have seen dramatic developments in algorithmic techniques, and today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas. A surprising aspect of this development is that the best current SAT solvers are still to a large extent based on methods from the early 1960s, which can often handle formulas with millions of variables but may also get hopelessly stuck on formulas with just a few hundred variables. The fundamental question of when SAT solvers perform well or badly, and what underlying mathematical properties of the formulas influence SAT solver performance, remains very poorly understood. Another intriguing aspect is that much stronger mathematical methods of reasoning about propositional logic formulas are known today, in particular methods based on algebra and geometry, and these methods would seem to have great potential based on theoretical studies. However, attempts at harnessing the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. This workshop gathered leading researchers in applied and theoretical areas of SAT and computational complexity to stimulate an increased exchange of ideas between these two communities. We see great opportunities for fruitful interplay between theoretical and applied research in this area, and believe that this workshop showed beyond doubt that a more vigorous interaction between the two has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams. Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). In Dagstuhl Reports, Volume 5, Issue 4, pp. 98-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{biere_et_al:DagRep.5.4.98,
  author =	{Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordstr\"{o}m, Jakob and Williams, Ryan},
  title =	{{Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)}},
  pages =	{98--122},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordstr\"{o}m, Jakob and Williams, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.4.98},
  URN =		{urn:nbn:de:0030-drops-53520},
  doi =		{10.4230/DagRep.5.4.98},
  annote =	{Keywords: SAT, Boolean SAT solvers, SAT solving, conflict-driven clause learning, Gr\"{o}bner bases, pseudo-Boolean solvers, proof complexity, computational complexity, parameterized complexity}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.448
Tight Size-Degree Bounds for Sums-of-Squares Proofs

Authors: Massimo Lauria and Jakob Nordström

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size n^Omega(d) for values of d = d(n) from constant all the way up to n^delta for some universal constant delta. This shows that the n^O(d) running time obtained by using the Lasserre semidefinite programming relaxations to find degree-d SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NP-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in [Krajicek '04] and [Dantchev and Riis '03], and then applying a restriction argument as in [Atserias, Müller, and Oliva '13] and [Atserias, Lauria, and Nordstrom '14]. This yields a generic method of amplifying SOS degree lower bounds to size lower bounds, and also generalizes the approach in [ALN14] to obtain size lower bounds for the proof systems resolution, polynomial calculus, and Sherali-Adams from lower bounds on width, degree, and rank, respectively.
Cite as

Massimo Lauria and Jakob Nordström. Tight Size-Degree Bounds for Sums-of-Squares Proofs. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 448-466, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{lauria_et_al:LIPIcs.CCC.2015.448,
  author =	{Lauria, Massimo and Nordstr\"{o}m, Jakob},
  title =	{{Tight Size-Degree Bounds for Sums-of-Squares Proofs}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{448--466},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.448},
  URN =		{urn:nbn:de:0030-drops-50736},
  doi =		{10.4230/LIPIcs.CCC.2015.448},
  annote =	{Keywords: Proof complexity, resolution, Lasserre, Positivstellensatz, sums-of-squares, SOS, semidefinite programming, size, degree, rank, clique, lower bound}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.467
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

Authors: Mladen Miksa and Jakob Nordström

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We study the problem of establishing lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov '02], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution.
Cite as

Mladen Miksa and Jakob Nordström. A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 467-487, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{miksa_et_al:LIPIcs.CCC.2015.467,
  author =	{Miksa, Mladen and Nordstr\"{o}m, Jakob},
  title =	{{A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{467--487},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.467},
  URN =		{urn:nbn:de:0030-drops-50775},
  doi =		{10.4230/LIPIcs.CCC.2015.467},
  annote =	{Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, degree, size, functional pigeonhole principle, lower bound}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.300
From Small Space to Small Width in Resolution

Authors: Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation -- previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.
Cite as

Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. From Small Space to Small Width in Resolution. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 300-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.STACS.2014.300,
  author =	{Filmus, Yuval and Lauria, Massimo and Miksa, Mladen and Nordstr\"{o}m, Jakob and Vinyals, Marc},
  title =	{{From Small Space to Small Width in Resolution}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{300--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.300},
  URN =		{urn:nbn:de:0030-drops-44661},
  doi =		{10.4230/LIPIcs.STACS.2014.300},
  annote =	{Keywords: proof complexity, resolution, width, space, polynomial calculus, PCR}
}
Document
DOI: 10.4230/DagSemProc.08381.6
Understanding space in resolution: optimal lower bounds and exponential trade-offs

Authors: Eli Ben-Sasson and Jakob Nordström

Published in: Dagstuhl Seminar Proceedings, Volume 8381, Computational Complexity of Discrete Problems (2008)

Abstract
We continue the study of tradeoffs between space and length of resolution proofs and focus on two new results: begin{enumerate} item We show that length and space in resolution are uncorrelated. This is proved by exhibiting families of CNF formulas of size $O(n)$ that have proofs of length $O(n)$ but require space $Omega(n / log n)$. Our separation is the strongest possible since any proof of length $O(n)$ can always be transformed into a proof in space $O(n / log n)$, and improves previous work reported in [Nordstr"{o}m 2006, Nordstr"{o}m and H{aa}stad 2008]. item We prove a number of trade-off results for space in the range from constant to $O(n / log n)$, most of them superpolynomial or even exponential. This is a dramatic improvement over previous results in [Ben-Sasson 2002, Hertel and Pitassi 2007, Nordstr"{o}m 2007]. end{enumerate} The key to our results is the following, somewhat surprising, theorem: Any CNF formula $F$ can be transformed by simple substitution transformation into a new formula $F'$ such that if $F$ has the right properties, $F'$ can be proven in resolution in essentially the same length as $F$ but the minimal space needed for $F'$ is lower-bounded by the number of variables that have to be mentioned simultaneously in any proof for $F$. Applying this theorem to so-called pebbling formulas defined in terms of pebble games over directed acyclic graphs and analyzing black-white pebbling on these graphs yields our results.
Cite as

Eli Ben-Sasson and Jakob Nordström. Understanding space in resolution: optimal lower bounds and exponential trade-offs. In Computational Complexity of Discrete Problems. Dagstuhl Seminar Proceedings, Volume 8381, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bensasson_et_al:DagSemProc.08381.6,
  author =	{Ben-Sasson, Eli and Nordstr\"{o}m, Jakob},
  title =	{{Understanding space in resolution: optimal lower bounds and exponential trade-offs}},
  booktitle =	{Computational Complexity of Discrete Problems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8381},
  editor =	{Peter Bro Miltersen and R\"{u}diger Reischuk and Georg Schnitger and Dieter van Melkebeek},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08381.6},
  URN =		{urn:nbn:de:0030-drops-17815},
  doi =		{10.4230/DagSemProc.08381.6},
  annote =	{Keywords: Proof complexity, Resolution, Pebbling.}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact