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
Proof Complexity Zoo - https://proofcomplexityzoo.gitlab.io/zoo/
cluster_extFrege
cluster_notpolybounded
Not poly bounded
cluster_tlRes
cluster_SA
cluster_Res
cluster_Res(LP)
cluster_PSC
cluster_Frege
cluster_uRes(CP)
extFrege
extFrege
extRes
extRes
extFrege->extRes
Frege
Frege
extFrege->Frege
tlRes
tlRes
hit
hit
tlRes->hit
ttp
ttp
tlRes->ttp
ordRes
ordRes
tlRes->ordRes
SA
SA
circRes
circRes
SA->circRes
uSA
uSA
SA->uSA
NS_Q
NS_Q
SA->NS_Q
tlResLin_F2
tlResLin_F2
SA->tlResLin_F2
PC_Q
PC_Q
SA->PC_Q
Res
Res
circRes->Res
saturationCP
saturationCP
Res->saturationCP
poolRes
poolRes
Res->poolRes
linRes
linRes
Res->linRes
revRes
revRes
Res->revRes
Res->uSA
regRes
regRes
poolRes->regRes
linRes->tlRes
linRes->regRes
revRes->tlRes
uSA->revRes
tlCP
tlCP
ordRes->tlCP
NS_F2
NS_F2
ordRes->NS_F2
ordRes->NS_Q
regRes->tlRes
regRes->ordRes
tlCP->tlRes
NS_F2->tlRes
SoS
SoS
NS_F2->SoS
AC0Frege
AC0Frege
NS_F2->AC0Frege
NS_Q->tlRes
NS_Q->AC0Frege
CP
CP
CP->tlCP
CP->NS_F2
CP->NS_Q
uSP
uSP
CP->uSP
CP->SoS
Res-k
Res-k
CP->Res-k
uCP
uCP
uSP->uCP
SoS->SA
SoS->PC_Q
sLSn+
sLSn+
SoS->sLSn+
Res-k->Res
PC_F2
PC_F2
uCP->PC_F2
uCP->tlResLin_F2
uCP->PC_Q
uL&P
uL&P
uCP->uL&P
uCP->AC0Frege
PC_F2->SA
PC_F2->Res
PC_F2->NS_F2
sLS+
sLS+
PC_F2->sLS+
tlResLin_F2->tlRes
PC_Q->Res
PC_Q->NS_Q
uL&P->Res
AC0Frege->Res-k
semanticCP
semanticCP
semanticCP->CP
semanticCP->sLSn+
sLSn+->sLS+
L&P
L&P
sLSn+->L&P
SP
SP
SP->CP
SP->sLSn+
tlTH(k)
tlTH(k)
tlTH(k)->tlCP
tlLSd+
tlLSd+
tlTH(k)->tlLSd+
tlLS+
tlLS+
tlLSd+->tlLS+
sLS+->tlResLin_F2
sLS+->PC_Q
sLS+->AC0Frege
sLS+->tlLS+
sLS
sLS
sLS+->sLS
regResLin_F2
regResLin_F2
regResLin_F2->tlResLin_F2
L&P->uL&P
tlLS
tlLS
tlLS->tlRes
tlLS+->tlLS
sLS->tlLS
OBDDjoinweak
OBDDjoinweak
OBDDjoinweak->SoS
OBDDjoinweak->uCP
OBDDjoinweak->semanticCP
OBDDjoinweak->SP
OBDDjoinweak->L&P
Res(LP)
Res(LP)
Res(L&P)
Res(L&P)
Res(LP)->Res(L&P)
uRes(LP)
uRes(LP)
Res(LP)->uRes(LP)
Res(L&P)->L&P
PSC
PSC
PS
PS
PSC->PS
PS->SoS
LK
LK
Frege->LK
TC0Frege
TC0Frege
Frege->TC0Frege
uRes(CP)
uRes(CP)
uRes(CP)->uSP
uRes(CP)->SoS
uRes(CP)->uRes(LP)
uRes(LP)->Res-k
uRes(L&P)
uRes(L&P)
uRes(LP)->uRes(L&P)
Res(CP)
Res(CP)
Res(CP)->SP
Res(CP)->Res(LP)
ResLin_Z
ResLin_Z
uResLin_Z
uResLin_Z
ResLin_Z->uResLin_Z
uResLin_Z->uRes(CP)
ResLin_F2
ResLin_F2
uResLin_Z->ResLin_F2
ResLin_F2->Res
ResLin_F2->SoS
ResLin_F2->AC0Frege
ResLin_F2->regResLin_F2
LS
LS
LS->PC_F2
LS->tlResLin_F2
LS->PC_Q
LS->AC0Frege
LS->L&P
LS->tlLS
LS+
LS+
LS+->tlLS+
LS+->LS
LSd+
LSd+
LSd+->SoS
LSd+->semanticCP
LSd+->SP
LSd+->tlLSd+
LSd+->L&P
LSd+->LS+
LSn+
LSn+
LSn+->PSC
LSn+->LSd+
CPS
CPS
CPS->LSn+
IPS
IPS
CPS->IPS
IPS->extFrege
TC0Frege->Res(CP)
AC0(+)Frege
AC0(+)Frege
TC0Frege->AC0(+)Frege
AC0(+)Frege->PC_F2
AC0(+)Frege->ResLin_F2
AC0Frege+Mod2axioms
AC0Frege+Mod2axioms
AC0(+)Frege->AC0Frege+Mod2axioms
AC0Frege+Mod2axioms->NS_F2
AC0Frege+Mod2axioms->AC0Frege
ZFC
ZFC
ZFC->extFrege
separation
simulation
sim+sep
equivalence
incomparability
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\))
Regular ResLin over \(\mathbb{F}_2\), regular 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
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.
Lower bounds for regular resolution over parities.
This database is still incomplete; missing data may indicate either the information was not yet recorded or an open problem. Users are encouraged to contribute missing proof systems and/or relations at https://gitlab.com/proofcomplexityzoo/zoo .