Workshop on Proof Complexity 2026

The workshop will be part of FLoC 2026 and affiliated with the conference SAT'26.

Invited talks

• Noah Fleming (University of Lund):
  Provable reductions

  Consider the following algorithm for finding a falsified clause of an unsatisfiable CNF formula, given an assignment: sequentially check each clause to see if it is falsified. As the formula is unsatisfiable, the algorithm clearly finds a falsified clause. However, proving that this algorithm is correct (outputs a falsified clause on every unsatisfiable CNF formula) is tantamount to showing NP=coNP! In this talk we will look at provably correct algorithms which find falsified clauses for subsets of unsatisfiable formulas, and show that these are equivalent to certain strong proof systems. Doing so will allow us to prove that two strong, and seemingly different, proof systems G1 and implicit resolution are polynomially equivalent, and develop a theory of provable reductions in TFNP.

• Jan Pich (University of Oxford):
  Limits of Lifting

  Over the past decade, lifting theorems have become one of the most popular frameworks for proving complexity lower bounds. Along the way, the method established a strong connection between proof complexity and monotone circuit complexity. But what is its real potential? Can lifting be used to obtain, for instance, monotone circuit lower bounds for slice functions and general non-monotone circuit lower bounds separating P and NP? The aim of this talk is to clarify the inherent limitations of this approach. This is joint work with Gaia Carenini, Bruno Cavalar and Stefan Grosser.

• Benjamin Böhm (University of Jena): invited speaker in the joint session with the QBF workshop
  The Complexity of Quantified CDCL

  Solving Quantified Boolean Formulas (QBFs) extends the well-known SAT problem by allowing quantification over variables. As the canonical PSPACE-complete problem, QBF is generally considered to be significantly harder than the NP-complete SAT problem. Despite the absence of polynomial-time algorithms for SAT, the dominant practical approach, Conflict Driven Clause Learning (CDCL), performs remarkably well on many industrial instances. For unsatisfiable formulas, CDCL generates Resolution refutations, and a result by Pipatsrisawat and Darwiche (2011) established that CDCL, viewed as a proof system, is equivalent to Resolution.

  A common strategy in QBF solving is to lift successful SAT-solving techniques to the quantified setting. In particular, CDCL can be generalized to Quantified Conflict Driven Clause Learning (QCDCL). In this talk, we examine the similarities and differences between CDCL and QCDCL. We identify limitations of QCDCL by applying exponential lower bounds and use these results to compare and separate different QCDCL variants. A central question is whether there exists a variant of QCDCL that simulates its underlying proof system in the same way that CDCL simulates Resolution. We present several modifications of QCDCL and show how they can strengthen the framework and potentially improve its performance compared to the standard version widely used in practice.

• Dmitry Sokolov (University of Montreal):
  Lower Bounds via Friedman-Pippenger Technique

  Friedman-Pippenger technique is a powerful tool for building embeddings between graphs. It is quite popular in combinatorics and discrete mathematics for showing the existence of subgraphs, minors, etc. in expanders. We discuss recent "dynamic" versions of the considered technique. As an application, we show that resolution cannot efficiently certify the non-existence of Hamiltonian cycles in constant-degree graphs.

Contributed Talks

• Toward a Characterization of Simulation Between Arithmetic Theories (Hunter Monroe)
• Lower Bounds against the Ideal Proof System in Finite Fields (Tal Elbaz, Nashlen Govindasamy, Jiaqi Lu, Iddo Tzameret)
• A Boolean static proof system for Quantified Boolean Formulas (Jan Johannsen, Marc Vinyals)
• Cardinality Cuts & Saturation (Jake Anderson, Marc Vinyals, Massimo Lauria, Wietze Koops)
• Towards a positive version of Cook’s PV (Adriana Baldacchino, Anupam Das)
• Proof Systems Based on Structured Circuits (Matthäus Micun, Christoph Berkholz)
• Symmetric Proofs in the Ideal Proof System (Anuj Dawar)
• Size-degree inequalities in Sherali-Adams and Sum-of-Squares made simple (Ilario Bonacina)
• Cardinality Constraints are Hard for Resolution (Ilario Bonacina, Jordi Levy, Ion Mikel Liberal)

Important dates

• 15 May 2026 Abstract submission
• 20 May 2026 Notification to authors
• 1 June 2026 Early registration deadline
• 18-19 July 2026 Workshop in Lisbon

Scope

Proof complexity is the study of the complexity of theorem proving procedures. The central question in proof complexity is: given a theorem F (e.g. a propositional tautology) and a proof system P (i.e., a formalism usually comprised of axioms and rules), what is the size of the smallest proof of F in the system P? Moreover, how difficult is it to construct a small proof? Many ingenious techniques have been developed to try to answer these questions, which bare tight relations to intricate theoretical open problems from computational complexity (such as the celebrated P vs. NP problem), mathematical logic (e.g. separating theories of Bounded Arithmetic) as well as to practical problems in SAT solving.

Submissions

We welcome submissions of abstracts based on work which may be submitted or published elsewhere, provided that this information is disclosed at submission time. There will be no formal reviewing. The organisers will check relevance and may provide additional feedback.

Abstracts are invited of ongoing, finished, or (if clearly stated) even recently published work on a topic relevant to the workshop. Abstracts (at most 2 pages) are to be submitted electronically in PDF via the submission site.

Accepted communications must be presented at the workshop by one of the authors.

Joint session with the QBF Workshop

As part of the workshop we plan a joint session with the International Workshop on Quantified Boolean Formulas and Beyond. Submissions on proof complexity of QBF (and other logics involving quantification) are very welcome.

Student travel bursaries available

Bursaries for travel support will be available for students, who want to attend the workshop and combine this with a visit to SAT. Details will be announced on the SAT'26 websites in due time.

Organisers

• Olaf Beyersdorff (University of Jena)
• Jan Johannsen (LMU Munich)
• Massimo Lauria (Sapienza Rome)

Registration

Registration for the workshop is mandatory, please see the information at FLOC. Early registration ends on 1 June 2026.