23 Search Results for "Nordstr�m, Jakob"


Document
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-dev.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
RANDOM
Bias Reduction for Sum Estimation

Authors: Talya Eden, Jakob Bæk Tejs Houen, Shyam Narayanan, Will Rosenbaum, and Jakub Tětek

Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)


Abstract
In classical statistics and distribution testing, it is often assumed that elements can be sampled exactly from some distribution 𝒫, and that when an element x is sampled, the probability 𝒫(x) of sampling x is also known. In this setting, recent work in distribution testing has shown that many algorithms are robust in the sense that they still produce correct output if the elements are drawn from any distribution 𝒬 that is sufficiently close to 𝒫. This phenomenon raises interesting questions: under what conditions is a "noisy" distribution 𝒬 sufficient, and what is the algorithmic cost of coping with this noise? In this paper, we investigate these questions for the problem of estimating the sum of a multiset of N real values x_1, …, x_N. This problem is well-studied in the statistical literature in the case 𝒫 = 𝒬, where the Hansen-Hurwitz estimator [Annals of Mathematical Statistics, 1943] is frequently used. We assume that for some (known) distribution 𝒫, values are sampled from a distribution 𝒬 that is pointwise close to 𝒫. That is, there is a parameter γ < 1 such that for all x_i, (1 - γ) 𝒫(i) ≤ 𝒬(i) ≤ (1 + γ) 𝒫(i). For every positive integer k we define an estimator ζ_k for μ = ∑_i x_i whose bias is proportional to γ^k (where our ζ₁ reduces to the classical Hansen-Hurwitz estimator). As a special case, we show that if 𝒬 is pointwise γ-close to uniform and all x_i ∈ {0, 1}, for any ε > 0, we can estimate μ to within additive error ε N using m = Θ(N^{1-1/k}/ε^{2/k}) samples, where k = ⌈lg ε/lg γ⌉. We then show that this sample complexity is essentially optimal. Interestingly, our upper and lower bounds show that the sample complexity need not vary uniformly with the desired error parameter ε: for some values of ε, perturbations in its value have no asymptotic effect on the sample complexity, while for other values, any decrease in its value results in an asymptotically larger sample complexity.

Cite as

Talya Eden, Jakob Bæk Tejs Houen, Shyam Narayanan, Will Rosenbaum, and Jakub Tětek. Bias Reduction for Sum Estimation. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 62:1-62:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{eden_et_al:LIPIcs.APPROX/RANDOM.2023.62,
  author =	{Eden, Talya and Houen, Jakob B{\ae}k Tejs and Narayanan, Shyam and Rosenbaum, Will and T\v{e}tek, Jakub},
  title =	{{Bias Reduction for Sum Estimation}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{62:1--62:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.62},
  URN =		{urn:nbn:de:0030-drops-188872},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.62},
  annote =	{Keywords: bias reduction, sum estimation, sublinear time algorithms, sample complexity}
}
Document
Track A: Algorithms, Complexity and Games
A Sparse Johnson-Lindenstrauss Transform Using Fast Hashing

Authors: Jakob Bæk Tejs Houen and Mikkel Thorup

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)


Abstract
The Sparse Johnson-Lindenstrauss Transform of Kane and Nelson (SODA 2012) provides a linear dimensionality-reducing map A ∈ ℝ^{m × u} in 𝓁₂ that preserves distances up to distortion of 1 + ε with probability 1 - δ, where m = O(ε^{-2} log 1/δ) and each column of A has O(ε m) non-zero entries. The previous analyses of the Sparse Johnson-Lindenstrauss Transform all assumed access to a Ω(log 1/δ)-wise independent hash function. The main contribution of this paper is a more general analysis of the Sparse Johnson-Lindenstrauss Transform with less assumptions on the hash function. We also show that the Mixed Tabulation hash function of Dahlgaard, Knudsen, Rotenberg, and Thorup (FOCS 2015) satisfies the conditions of our analysis, thus giving us the first analysis of a Sparse Johnson-Lindenstrauss Transform that works with a practical hash function.

Cite as

Jakob Bæk Tejs Houen and Mikkel Thorup. A Sparse Johnson-Lindenstrauss Transform Using Fast Hashing. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 76:1-76:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{houen_et_al:LIPIcs.ICALP.2023.76,
  author =	{Houen, Jakob B{\ae}k Tejs and Thorup, Mikkel},
  title =	{{A Sparse Johnson-Lindenstrauss Transform Using Fast Hashing}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{76:1--76:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.76},
  URN =		{urn:nbn:de:0030-drops-181281},
  doi =		{10.4230/LIPIcs.ICALP.2023.76},
  annote =	{Keywords: dimensionality reduction, hashing, concentration bounds, moment bounds}
}
Document
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-dev.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
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-dev.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
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-dev.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
Proof Complexity of Natural Formulas via Communication Arguments

Authors: Dmitry Itsykson and Artur Riazanov

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


Abstract
A canonical communication problem Search(φ) is defined for every unsatisfiable CNF φ: an assignment to the variables of φ is partitioned among the communicating parties, they are to find a clause of φ falsified by this assignment. Lower bounds on the randomized k-party communication complexity of Search(φ) in the number-on-forehead (NOF) model imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula φ in the semantic proof system T^{cc}(k,c) that operates with proof lines that can be computed by k-party randomized communication protocol using at most c bits of communication [Göös and Pitassi, 2014]. All known lower bounds on Search(φ) (e.g. [Beame et al., 2007; Göös and Pitassi, 2014; Russell Impagliazzo et al., 1994]) are realized on ad-hoc formulas φ (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas. First, we demonstrate our approach for two-party communication and apply it to the proof system Res(⊕) that operates with disjunctions of linear equalities over 𝔽₂ [Dmitry Itsykson and Dmitry Sokolov, 2014]. Let a formula PM_G encode that a graph G has a perfect matching. If G has an odd number of vertices, then PM_G has a tree-like Res(⊕)-refutation of a polynomial-size [Dmitry Itsykson and Dmitry Sokolov, 2014]. It was unknown whether this is the case for graphs with an even number of vertices. Using our approach we resolve this question and show a lower bound 2^{Ω(n)} on size of tree-like Res(⊕)-refutations of PM_{K_{n+2,n}}. Then we apply our approach for k-party communication complexity in the NOF model and obtain a Ω(1/k 2^{n/2k - 3k/2}) lower bound on the randomized k-party communication complexity of Search(BPHP^{M}_{2ⁿ}) w.r.t. to some natural partition of the variables, where BPHP^{M}_{2ⁿ} is the bit pigeonhole principle and M = 2ⁿ+2^{n(1-1/k)}. In particular, our result implies that the bit pigeonhole requires exponential tree-like Th(k) proofs, where Th(k) is the semantic proof system operating with polynomial inequalities of degree at most k and k = 𝒪(log^{1-ε} n) for some ε > 0. We also show that BPHP^{2ⁿ+1}_{2ⁿ} superpolynomially separates tree-like Th(log^{1-ε} m) from tree-like Th(log m), where m is the number of variables in the refuted formula.

Cite as

Dmitry Itsykson and Artur Riazanov. Proof Complexity of Natural Formulas via Communication Arguments. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 3:1-3:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.CCC.2021.3,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Proof Complexity of Natural Formulas via Communication Arguments}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{3:1--3:34},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.3},
  URN =		{urn:nbn:de:0030-drops-142773},
  doi =		{10.4230/LIPIcs.CCC.2021.3},
  annote =	{Keywords: bit pigeonhole principle, disjointness, multiparty communication complexity, perfect matching, proof complexity, randomized communication complexity, Resolution over linear equations, tree-like proofs}
}
Document
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-dev.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
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-dev.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
A Syntax for Mutual Inductive Families

Authors: Ambrus Kaposi and Jakob von Raumer

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)


Abstract
Inductive families of types are a feature of most languages based on dependent types. They are usually described either by syntactic schemes or by encodings of strictly positive functors such as combinator languages or containers. The former approaches are informal and give only external signatures, the latter approaches suffer from encoding overheads and do not directly represent mutual types. In this paper we propose a direct method for describing signatures for mutual inductive families using a domain-specific type theory. A signature is a context (roughly speaking, a list of types) in this small type theory. Algebras, displayed algebras and sections are defined by models of this type theory: the standard model, the logical predicate and a logical relation interpretation, respectively. We reduce the existence of initial algebras for these signatures to the existence of the syntax of our domain-specific type theory. As this theory is very simple, its normal syntax can be encoded using indexed W-types. To the best of our knowledge, this is the first formalisation of the folklore fact that mutual inductive types can be reduced to indexed W-types. The contents of this paper were formalised in the proof assistant Agda.

Cite as

Ambrus Kaposi and Jakob von Raumer. A Syntax for Mutual Inductive Families. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2020.23,
  author =	{Kaposi, Ambrus and von Raumer, Jakob},
  title =	{{A Syntax for Mutual Inductive Families}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.23},
  URN =		{urn:nbn:de:0030-drops-123451},
  doi =		{10.4230/LIPIcs.FSCD.2020.23},
  annote =	{Keywords: type theory, inductive types, mutual inductive types, W-types, Agda}
}
Document
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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}
}
  • Refine by Author
  • 17 Nordström, Jakob
  • 4 Lauria, Massimo
  • 4 de Rezende, Susanna F.
  • 3 Sokolov, Dmitry
  • 2 Biere, Armin
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Proof complexity
  • 3 Theory of computation → Discrete optimization
  • 3 Theory of computation → Logic and verification
  • 1 Computing methodologies → Representation of polynomials
  • 1 Hardware → Theorem proving and SAT solving
  • Show More...

  • Refine by Keyword
  • 11 proof complexity
  • 6 resolution
  • 4 Proof complexity
  • 4 polynomial calculus
  • 3 Nullstellensatz
  • Show More...

  • Refine by Type
  • 23 document

  • Refine by Publication Year
  • 4 2023
  • 3 2015
  • 3 2020
  • 2 2017
  • 2 2021
  • Show More...

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