Proof Complexity Zoo

The Proof Complexity Zoo is a community-editable database of proof systems, formulas, and relations among them. The project is in its initial stage, and suggestions on which data to store, which queries to support, and how to present the information are particularly welcome. The database is user maintained and can be edited at https://gitlab.com/proofcomplexityzoo/zoo/-/edit/master/zoo.yaml after creating a user account on Gitlab and asking for editing permissions.

Settings

Quasipolynomial simulations / Quasipolynomial separations

Diagrams

• Minimal diagram
• Raw relations (for debugging purposes)

Proof Systems

• Resolution
• Truth table
• Tree-like resolution
• Regular resolution
• Ordered resolution
• Pool resolution
• Linear resolution
• Reversible resolution
• Cutting Planes
• Tree-like Cutting Planes
• Cutting Planes with Unary Coefficients
• Semantic Cutting Planes
• Cutting Planes with Saturation
• Stabbing Planes
• Stabbing Planes with Unary Coefficients
• Res(CP)
• Res(LP)
• Res(CP) with unary coefficients
• Res(LP) with unary coefficients
• Res(L\(\&\)P)
• Res(L\(\&\)P) with unary coefficients
• Semantic degree-k threshold system, treelike version
• Polynomial Calculus over \(\mathbb{F}_2\)
• Nullstellensatz over \(\mathbb{F}_2\)
• ResLin over \(\mathbb{Q}\), ResLin, Resolution over linear equations over rationals
• unary ResLin over \(\mathbb{Q}\), ResLin, Resolution over linear equations over rationals
• ResLin over \(\mathbb{F}_2\), Res(\(\oplus\))
• Tree-like ResLin over \(\mathbb{F}_2\), treelike Res(\(\oplus\))
• Polynomial Calculus over \(\mathbb{Q}\)
• Nullstellensatz over \(\mathbb{Q}\)
• Hitting
• Lift and Project
• Lift and Project with unary coefficients
• Positivstellensatz Calculus
• Positivstellensatz
• Lovász--Schrijver (LS)
• Lovász--Schrijver with squares (LS\(_+\))
• Lovász--Schrijver with squares (LS\(_+^d\)), bounded degree
• Lovász--Schrijver with squares (LS\(_+^\infty\)), unbounded degree
• Cone Proof System
• tl Lovász--Schrijver (LS)
• Lovász--Schrijver with squares (LS\(_+\))
• Lovász--Schrijver with squares (LS\(_+^d\)), bounded degree, treelike
• static Lovász--Schrijver (static LS)
• static Lovász--Schrijver, with squares of linear functions (static LS\(_+\))
• static Lovász--Schrijver, with squares of linear functions (static LS\(_+^n\))
• Sum of Squares (Lasserre)
• Sherali--Adams
• Circular resolution
• Unary Sherali--Adams
• Ideal Proof System
• Extended Frege
• Extended resolution
• Frege
• \(\mathrm{AC}^0\)-Frege
• k-DNF Resolution
• \(\mathrm{TC}^0\)-Frege
• \(\mathrm{AC}^0\)-Frege with mod 2 axioms
• \(\mathrm{AC}^0\)-Frege with mod 2 gates
• OBDD(join,weakening)
• LK
• Zermelo-Fraenkl Set Theory with the Axiom of Choice

Formulas

• Pigeonhole principle
• Pigeonhole principle with functionality axioms
• Pigeonhole principle with functionality and onto axioms
• Weak pigeonhole principle (2n pigeons, n holes)
• Weak pigeonhole principle (\(n^2\) pigeons, n holes)
• Bitwise pigeonhole principle
• Relativized pigeonhole principle (n,\(n^2\),n-1)
• Ordering principle
• Guarded ordering principle
• Tseitin over \(\mathbb{F}_2\)
• Tseitin over \(\mathbb{F}_2\) with k-ary AND gadget
• Tseitin over \(\mathbb{Q}\)
• Flow
• Tseitin \(\mathbb{F}_2\) \(\circ\) IND
• Tseitin \(\mathbb{Q}\) \(\circ\) IND
• Random CNF
• Clique-Colouring
• Clique-Colouring encoded as equalities
• Weak Clique-Colouring (2m clique, m colours)
• Weak Clique-Colouring (m^1/2 clique, log^2 m colours)
• Clique-Colouring composed with a permutation
• Pebbling \(\circ\) IND
• Pebbling \(\circ\) XOR, then guarded
• Stone formula
• String of pearls
• Sink of DAG \(\circ\) XOR

References

• The Relative Efficiency of Propositional Proof Systems.
• The Intractability of Resolution.
• Short Proofs for Tricky Formulas.
• Polynomial Size Proofs of the Propositional Pigeonhole Principle.
• Hard examples for resolution.
• Many Hard Examples for Resolution.
• Cutting plane versus Frege proof systems
• Exponential Lower Bounds for the Pigeonhole Principle.
• Independence in bounded arithmetic
• An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle
• More on the relative strength of counting principles.
• Short Resolution Proofs for a Sequence of Tricky Formulas.
• Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.
• None
• Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations.
• On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems.
• Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes.
• Exponential Incomparability of Tree-like and Ordered Resolution
• Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution.
• Hard examples for the bounded depth Frege proof system.
• Homogenization and the polynomial calculus.
• Lower Bounds for Polynomial Calculus: Non-Binomial Case.
• Constraint Propagation as a Proof System.
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning.
• Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations.
• An Exponential Separation between Regular and General Resolution.
• Rank Lower Bounds for the Sherali-Adams Operator.
• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams.
• A Near-Optimal Separation of Regular and General Resolution.
• Improved Separations of Regular Resolution from Clause Learning Proof Systems.
• Small Stone in Pool.
• Resolution over linear equations modulo two.
• Narrow Proofs May Be Maximally Long.
• On Linear Resolution.
• Semantic Versus Syntactic Cutting Planes.
• Random Formulas, Monotone Circuits, and Interpolation.
• The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs.
• Reordering Rule Makes OBDD Proof Systems Stronger.
• Stabbing Planes.
• Circuit Complexity, Proof Complexity, and Polynomial Identity Testing: The Ideal Proof System.
• Circular (Yet Sound) Proofs.
• Adventures in Monotone Complexity and TFNP.
• Proof complexity
• Semi-algebraic proofs, IPS lower bounds, and the τ-conjecture: can a natural number be negative?
• On the Complexity of Branching Proofs.
• Monotone Circuit Lower Bounds from Resolution.
• On the Power and Limitations of Branch and Cut.
• Separations in Proof Complexity and TFNP.
• Proving Unsatisfiability with Hitting Formulas.
• Sub-Exponential Lower Bounds for Branch-and-Bound with General Disjunctions via Interpolation
• Complexity of semialgebraic proofs
• Several notes on the power of Gomory-Chvátal cuts.
• On the complexity of the propositional calculus
• Lower bounds of static Lovász-Schrijver calculus proofs for Tseitin tautologies
• An Exponential Lower Bound on the Length of Some Classes of Branch-and-Cut Proofs.
• Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs.
• Lower Bounds for Lov[a-acute]sz--Schrijver Systems and Beyond Follow from Multiparty Communication Complexity.
• Resolution over linear equations and multilinear proofs.
• On the Lengths of Proofs in the Propositional Calculus
• Proof Complexity of Natural Formulas via Communication Arguments.