75 Search Results for "Nordström, Jakob"

Volume

LIPIcs, Volume 341

28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

SAT 2025, August 12-15, 2025, Glasgow, Scotland

Editors: Jeremias Berg and Jakob Nordström

Document
DOI: 10.4230/LIPIcs.SAT.2026.17
A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

Authors: Ruben Götz, Michael Dörr, and Dominik Schreiber

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Unsatisfiability proofs are valuable artifacts in propositional satisfiability (SAT) since they can provide correctness guarantees and thus complete trust in reported results. In powerful parallel and distributed clause-sharing SAT solvers, existing proof technology either funnels all solver threads' relevant reasoning steps into a single proof file, which leads to scalability problems for large setups and long running times, or checks proof information in parallel in real-time, which is fully scalable but leaves no persistent artifact. We suggest an alternative approach to achieve the best of both worlds. Specifically, we consider parallel proof files that are logged and also checked in parallel. To this end, we introduce PalRUP - an LRUP-based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components. In evaluations on up to 3072 cores, we observe that our approach allows for low-overhead proof logging during solving and substantially outscales prior proof producing approaches in terms of checking performance.
Cite as

Ruben Götz, Michael Dörr, and Dominik Schreiber. A Natively Parallel Proof Framework for Clause-Sharing SAT Solving. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gotz_et_al:LIPIcs.SAT.2026.17,
  author =	{G\"{o}tz, Ruben and D\"{o}rr, Michael and Schreiber, Dominik},
  title =	{{A Natively Parallel Proof Framework for Clause-Sharing SAT Solving}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.17},
  URN =		{urn:nbn:de:0030-drops-263239},
  doi =		{10.4230/LIPIcs.SAT.2026.17},
  annote =	{Keywords: Satisfiability, Proofs, Distributed computing}
}
Artifact
Software
DOI: 10.4230/artifacts.26901
VeriPB

Authors: Andy Oertel and Ciaran McCreesh

Abstract
Cite as

Andy Oertel, Ciaran McCreesh. VeriPB (Software, VeriPB). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26901,
   title = {{VeriPB}}, 
   author = {Oertel, Andy and McCreesh, Ciaran},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:rev:6d38dab246af9c321b8f17cb5a187f2fbb9e491d}{\texttt{swh:1:rev:6d38dab246af9c321b8f17cb5a187f2fbb9e491d}} (visited on 2026-07-13)},
   url = {https://gitlab.com/MIAOresearch/software/VeriPB},
   doi = {10.4230/artifacts.26901},
}
Artifact
Software
DOI: 10.4230/artifacts.26902
CakePB

Authors: Yong Kiam Tan

Abstract
Cite as

Yong Kiam Tan. CakePB (Software, CakePB). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26902,
   title = {{CakePB}}, 
   author = {Tan, Yong Kiam},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:rev:a7593ef22de2fc0b47a688f2d4f08e6b742735af}{\texttt{swh:1:rev:a7593ef22de2fc0b47a688f2d4f08e6b742735af}} (visited on 2026-07-13)},
   url = {https://gitlab.com/MIAOresearch/software/cakepb},
   doi = {10.4230/artifacts.26902},
}
Document
DOI: 10.4230/LIPIcs.CP.2026.21
End-to-End Certified Graph Colouring

Authors: Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs an ever more serious concern. The most promising remedy is to make solvers certifying, so that they use proof logging to generate machine-verifiable proofs of correctness. We present the first example of state-of-the-art certified graph colouring by equipping the solver ZykovColor with VeriPB proof logging. Combined with the formally verified CakePB checker, this provides end-to-end formally certified results. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking.
Cite as

Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-End Certified Graph Colouring. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dold_et_al:LIPIcs.CP.2026.21,
  author =	{Dold, Simon and Katsirelos, George and Koops, Wietze and Myreen, Magnus O. and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam},
  title =	{{End-to-End Certified Graph Colouring}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{21:1--21:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.21},
  URN =		{urn:nbn:de:0030-drops-266546},
  doi =		{10.4230/LIPIcs.CP.2026.21},
  annote =	{Keywords: graph colouring, proof logging, certifying algorithms}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.43
Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB

Authors: Ciaran McCreesh, Jakob Nordström, Andy Oertel, and Yong Kiam Tan

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
When a certifying solver claims that a solution is optimal or that a problem is unsatisfiable, it demonstrates this convincingly by giving a proof log which can be checked by an independent (and ideally formally verified) proof checker. Such an approach should also be viable for enumeration problems ("I have listed all solutions explicitly") and counting problems ("there are exactly 42 solutions"), but the currently most popular proof logging systems contain several vital features which are incompatible with this goal. We explain how the VeriPB system can be modified for enumeration and counting proofs whilst retaining as much as possible of its powerful "strengthening" and "deletion" features. We implement this extension both inside VeriPB’s user-friendly proof checker and elaborator and the formally verified CakePB backend, and use this to obtain formally verified enumerations of solutions for a range of constraint solving and graph problem instances.
Cite as

Ciaran McCreesh, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mccreesh_et_al:LIPIcs.CP.2026.43,
  author =	{McCreesh, Ciaran and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam},
  title =	{{Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{43:1--43:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.43},
  URN =		{urn:nbn:de:0030-drops-266759},
  doi =		{10.4230/LIPIcs.CP.2026.43},
  annote =	{Keywords: Constraint programming, proof logging, auditable solving}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.38
Solving Small Rubik’s Cubes as Slowly as Possible

Authors: Jenny Quan, Noah Kim, Bernardo Subercaseaux, and John Mackey

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
We study, for different Rubik’s puzzles, whether from any starting state one can solve the puzzle as slowly as possible, visiting every reachable state exactly once before reaching the solved configuration. This question corresponds to the existence of Hamiltonian paths (ending in the solved state) in the Cayley graphs associated with these puzzles. A major conjecture attributed to Lovász is that every Cayley graph has a Hamiltonian path. An even stronger version of the conjecture, considered by Dupuis and Wagon (2015) and Gregor et al. (2024), is that every Cayley graph of degree at least 3 is either bipartite and has Hamiltonian paths between any pair of vertices on opposite parts, or is non-bipartite and has Hamiltonian paths between any pair of vertices. Our study of slowly solving Rubik’s puzzles amounts to studying this Strong Lovász Conjecture in their respective Cayley graphs. We first verify the Strong Lovász Conjecture computationally for small Rubik’s puzzles like the 1 × 2 × 3 or 1 × 3 × 3 cuboids, which have under 200 states. This approach, however, becomes infeasible for the 2 × 2 × 2, which has over 3.6 million states. Our main result is then showing that the Strong Lovász Conjecture holds for the 2 × 2 × 2 cube, using a careful graph-theoretic construction based on the subgroup induced by the R and U turns.
Cite as

Jenny Quan, Noah Kim, Bernardo Subercaseaux, and John Mackey. Solving Small Rubik’s Cubes as Slowly as Possible. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{quan_et_al:LIPIcs.FUN.2026.38,
  author =	{Quan, Jenny and Kim, Noah and Subercaseaux, Bernardo and Mackey, John},
  title =	{{Solving Small Rubik’s Cubes as Slowly as Possible}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.38},
  URN =		{urn:nbn:de:0030-drops-257570},
  doi =		{10.4230/LIPIcs.FUN.2026.38},
  annote =	{Keywords: Hamilton connectivity, Rubik’s Cube, Finite group theory}
}
Document
DOI: 10.4230/DagRep.15.6.1
Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)

Authors: Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, and Wietze Koops

Published in: Dagstuhl Reports, Volume 15, Issue 6 (2026)

Abstract
Modern automated reasoning has transformed large parts of industry and has also found numerous scientific applications. But many reasoning problems are computationally very challenging, or sometimes even undecidable. Because of this, the reasoning algorithms used are often very complex, and even the best current algorithms at times produce wrong results. As these tools are increasingly being used autonomously, sometimes even in life-critical applications, it is urgent to ensure that what they compute is valid. Software testing, while immensely useful, cannot guarantee correctness, and state-of-the-art algorithms are far beyond what techniques for producing formally verified software can handle. The focus of this Dagstuhl Seminar was the approach of addressing such issues by designing certifying algorithms using so-called proof logging, meaning that algorithms output not only a result but also a machine-verifiable proof of correctness. This proof can then be fed to a dedicated proof checker for verification. Crucially, such proofs should require low overhead to generate and be easy to check, but still supply 100% correctness guarantees. Besides ensuring correctness of outputs for complex algorithms, proof logging can also provide new tools for algorithm development and analysis, software debugging, and even research into explainability in the context of AI.
Cite as

Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, and Wietze Koops. Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231). In Dagstuhl Reports, Volume 15, Issue 6, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.15.6.1,
  author =	{Bj{\o}rner, Nikolaj S. and Heule, Marijn J. H. and Kaufmann, Daniela and Nordstr\"{o}m, Jakob and Koops, Wietze},
  title =	{{Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)}},
  pages =	{1--31},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{6},
  editor =	{Bj{\o}rner, Nikolaj S. and Heule, Marijn J. H. and Kaufmann, Daniela and Nordstr\"{o}m, Jakob and Koops, Wietze},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.6.1},
  URN =		{urn:nbn:de:0030-drops-255798},
  doi =		{10.4230/DagRep.15.6.1},
  annote =	{Keywords: ATP, Computer Algebra, DRAT, DRUP, MIP, Propagation Redundancy, QBF, SAT, SMT}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.81
Supercritical Tradeoff Between Size and Depth for Resolution over Parities

Authors: Dmitry Itsykson and Alexander Knop

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res(⊕)) refutation must either have exponential size (in the formula size) or superlinear depth (in the number of variables). In this paper, we extend this result by constructing a formula with the same hardness properties, but which additionally admits a resolution refutation of quasi-polynomial size. This establishes a supercritical tradeoff between size and depth for resolution over parities. The proof builds on the framework of Alekseev and Itsykson and relies on a lifting argument applied to the supercritical tradeoff between width and depth in resolution, proposed by Buss and Thapen (IPL 2026).
Cite as

Dmitry Itsykson and Alexander Knop. Supercritical Tradeoff Between Size and Depth for Resolution over Parities. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 81:1-81:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.ITCS.2026.81,
  author =	{Itsykson, Dmitry and Knop, Alexander},
  title =	{{Supercritical Tradeoff Between Size and Depth for Resolution over Parities}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{81:1--81:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  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.ITCS.2026.81},
  URN =		{urn:nbn:de:0030-drops-253680},
  doi =		{10.4230/LIPIcs.ITCS.2026.81},
  annote =	{Keywords: lifting theorems, resolution depth, resolution over parities, resolution width, supercritical tradeoff}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.60
Total Search Problems in ZPP

Authors: Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
We initiate a systematic study of TFZPP, the class of total NP search problems solvable by polynomial time randomized algorithms. TFZPP contains a variety of important search problems such as Bertrand-Chebyshev (finding a prime between N and 2N), refuter problems for many circuit lower bounds, and Lossy-Code. The Lossy-Code problem has found prominence due to its fundamental connections to derandomization, catalytic computing, and the metamathematics of complexity theory, among other areas. While TFZPP collapses to FP under standard derandomization assumptions in the white-box setting, we are able to separate TFZPP from the major TFNP subclasses in the black-box setting. In fact, we are able to separate it from every uniform TFNP class assuming that NP is not in quasi-polynomial time. To do so, we extend the connection between proof complexity and black-box TFNP to randomized proof systems and randomized reductions. Next, we turn to developing a taxonomy of TFZPP problems. We highlight a problem called Nephew, originating from an infinity axiom in set theory. We show that Nephew is in PWPP∩ TFZPP and conjecture that it is not reducible to Lossy-Code. Intriguingly, except for some artificial examples, most other black-box TFZPP problems that we are aware of reduce to Lossy-Code: - We define a problem called Empty-Child capturing finding a leaf in a rooted (binary) tree, and show that this problem is equivalent to Lossy-Code. We also show that a variant of Empty-Child with "heights" is complete for the intersection of SOPL and Lossy-Code. - We strengthen Lossy-Code with several combinatorial inequalities such as the AM-GM inequality. Somewhat surprisingly, we show the resulting new problems are still reducible to Lossy-Code. A technical highlight of this result is that they are proved by formalizations in bounded arithmetic, specifically in Jeřábek’s theory APC₁ (JSL 2007). - Finally, we show that the Dense-Linear-Ordering problem reduces to Lossy-Code.
Cite as

Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan. Total Search Problems in ZPP. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 60:1-60:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.ITCS.2026.60,
  author =	{Fleming, Noah and Grosser, Stefan and Jain, Siddhartha and Li, Jiawei and Ren, Hanlin and Shirley, Morgan and Yuan, Weiqiang},
  title =	{{Total Search Problems in ZPP}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{60:1--60:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  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.ITCS.2026.60},
  URN =		{urn:nbn:de:0030-drops-253473},
  doi =		{10.4230/LIPIcs.ITCS.2026.60},
  annote =	{Keywords: TFNP, lossy code, randomized proof systems, query complexity}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.111
Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits

Authors: Hanlin Ren, Yichuan Wang, and Yan Zhong

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
Given a circuit G: {0, 1}ⁿ → {0, 1}^m with m > n, the range avoidance problem (Avoid) asks to output a string y ∈ {0, 1}^m that is not in the range of G. Besides its profound connection to circuit complexity and explicit construction problems, this problem is also related to the existence of proof complexity generators - circuits G: {0, 1}ⁿ → {0, 1}^m where m > n but for every y ∈ {0, 1}^m, it is infeasible to prove the statement "y ̸ ∈ Range(G)" in a given propositional proof system. This paper connects these two problems with the existence of demi-bits generators, a fundamental cryptographic primitive against nondeterministic adversaries introduced by Rudich (RANDOM '97). - We show that the existence of demi-bits generators implies Avoid is hard for nondeterministic algorithms. This resolves an open problem raised by Chen and Li (STOC '24). Furthermore, assuming the demi-hardness of certain LPN-style generators or Goldreich’s PRG, we prove the hardness of Avoid even when the instances are constant-degree polynomials over 𝔽₂. - We show that the dual weak pigeonhole principle is unprovable in Cook’s theory PV₁ under the existence of demi-bits generators secure against AM/_{O(1)}, thereby separating Jeřábek’s theory APC₁ from PV₁. Previously, Ilango, Li, and Williams (STOC '23) obtained the same separation under different (and arguably stronger) cryptographic assumptions. - We transform demi-bits generators to proof complexity generators that are pseudo-surjective in certain parameter regime. Pseudo-surjectivity is the strongest form of hardness considered in the literature for proof complexity generators. Our constructions are inspired by the recent breakthroughs on the hardness of Avoid by Ilango, Li, and Williams (STOC '23) and Chen and Li (STOC '24). We use randomness extractors to significantly simplify the construction and the proof.
Cite as

Hanlin Ren, Yichuan Wang, and Yan Zhong. Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 111:1-111:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ren_et_al:LIPIcs.ITCS.2026.111,
  author =	{Ren, Hanlin and Wang, Yichuan and Zhong, Yan},
  title =	{{Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{111:1--111:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  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.ITCS.2026.111},
  URN =		{urn:nbn:de:0030-drops-253982},
  doi =		{10.4230/LIPIcs.ITCS.2026.111},
  annote =	{Keywords: Range Avoidance, Proof Complexity Generators}
}
Document
PACE Solver Description
DOI: 10.4230/LIPIcs.IPEC.2025.37
PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving

Authors: André Schidler

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
This paper describes our hybrid MaxSAT and mixed integer programming approach for finding minimum hitting sets as submitted to the 2025 PACE challenge. We also discuss hitting set specific challenges, lower bounds, preprocessing and design choices.
Cite as

André Schidler. PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 37:1-37:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schidler:LIPIcs.IPEC.2025.37,
  author =	{Schidler, Andr\'{e}},
  title =	{{PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{37:1--37:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.37},
  URN =		{urn:nbn:de:0030-drops-251692},
  doi =		{10.4230/LIPIcs.IPEC.2025.37},
  annote =	{Keywords: hitting set, maxsat, core-guided}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.37
Communication Complexity of Equality and Error-Correcting Codes

Authors: Dale Jacobs, John Jeang, Vladimir Podolskii, Morgan Prior, and Ilya Volkovich

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We study the public-coin randomized communication complexity of the equality function. The communication complexity of this function is known to be low when the error probability is constant and the players have access to many random bits. The complexity grows, however, if the allowed error probability and the amount of randomness are restricted. We show that public-coin randomized protocols for equality and error-correcting codes are essentially the same object. That is, given a protocol for equality, we can construct a code, and vice versa. We substantially extend the protocol-implies-code direction: any protocol computing a function with a large fooling set can be converted into an error-correcting code. As a corollary, we show that among functions with a fooling set of size s, equality on log s bits has the least randomized communication complexity, regardless of the restrictions on the error probability and the amount of randomness. Finally, we use the connection to error-correcting codes to analyze the randomized communication complexity of equality for varying restrictions on the error probability and the amount of randomness. In most cases, we provide tight bounds. We pinpoint the setting in which tight bounds are still unknown.
Cite as

Dale Jacobs, John Jeang, Vladimir Podolskii, Morgan Prior, and Ilya Volkovich. Communication Complexity of Equality and Error-Correcting Codes. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jacobs_et_al:LIPIcs.FSTTCS.2025.37,
  author =	{Jacobs, Dale and Jeang, John and Podolskii, Vladimir and Prior, Morgan and Volkovich, Ilya},
  title =	{{Communication Complexity of Equality and Error-Correcting Codes}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.37},
  URN =		{urn:nbn:de:0030-drops-251175},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.37},
  annote =	{Keywords: communication complexity, randomized communication complexity, error-correcting codes}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.64
Searching for Falsified Clause in Random (log{n})-CNFs Is Hard for Randomized Communication

Authors: Artur Riazanov, Anastasia Sofronova, Dmitry Sokolov, and Weiqiang Yuan

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

Abstract
We show that for a randomly sampled unsatisfiable O(log n)-CNF over n variables the randomized two-party communication cost of finding a clause falsified by the given variable assignment is linear in n.
Cite as

Artur Riazanov, Anastasia Sofronova, Dmitry Sokolov, and Weiqiang Yuan. Searching for Falsified Clause in Random (log{n})-CNFs Is Hard for Randomized Communication. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 64:1-64:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{riazanov_et_al:LIPIcs.APPROX/RANDOM.2025.64,
  author =	{Riazanov, Artur and Sofronova, Anastasia and Sokolov, Dmitry and Yuan, Weiqiang},
  title =	{{Searching for Falsified Clause in Random (log\{n\})-CNFs Is Hard for Randomized Communication}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{64:1--64:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.64},
  URN =		{urn:nbn:de:0030-drops-244306},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.64},
  annote =	{Keywords: communication complexity, proof complexity, random CNF}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.18
Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

Authors: Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz [Jacobo Torán and Florian Wörz, 2023] showed that there is a resolution refutation of narrow width k for two graphs if and only if they can be distinguished in (k+1)-variable first-order logic (FO^{k+1}). While DAG-like narrow width k resolution refutations have size at most n^k, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width k but only in tree-like size 2^{Ω(n^{k/2})}. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical trade-off by Razborov [Alexander A. Razborov, 2016]. To prove our result, we develop a new variant of the k-pebble EF-game for FO^k to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer [Martin Grohe et al., 2023]. Using a recent improved robust compressed CFI construction of de Rezende, Fleming, Janett, Nordström, and Pang [Susanna F. de Rezende et al., 2024], we obtain a similar bound for width k (instead of the stronger but less common narrow width) and make the result more robust.
Cite as

Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2025.18,
  author =	{Berkholz, Christoph and Lichter, Moritz and Vinall-Smeeth, Harry},
  title =	{{Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{18:1--18:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.18},
  URN =		{urn:nbn:de:0030-drops-241253},
  doi =		{10.4230/LIPIcs.MFCS.2025.18},
  annote =	{Keywords: Proof complexity, Resolution, Width, Tree-like size, Supercritical trade-off, Lower bound, Finite model theory, CFI graphs}
}
  • Refine by Type
  • 72 Document/PDF
  • 39 Document/HTML
  • 2 Artifact
  • 1 Volume

  • Refine by Publication Year
  • 10 2026
  • 37 2025
  • 6 2024
  • 5 2023
  • 2 2022
  • Show More...

  • Refine by Author
  • 25 Nordström, Jakob
  • 8 Oertel, Andy
  • 7 de Rezende, Susanna F.
  • 6 Tan, Yong Kiam
  • 5 Berg, Jeremias
  • Show More...

  • Refine by Series/Journal
  • 67 LIPIcs
  • 4 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 22 Theory of computation → Proof complexity
  • 12 Theory of computation → Constraint and logic programming
  • 11 Theory of computation → Logic and verification
  • 9 Theory of computation → Automated reasoning
  • 9 Theory of computation → Discrete optimization
  • Show More...

  • Refine by Keyword
  • 16 proof complexity
  • 8 resolution
  • 7 Proof complexity
  • 7 proof logging
  • 5 certifying algorithms
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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