Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with reflection principles:
TR19-084 | 26th May 2019
Michal Garlik

Resolution Lower Bounds for Refutation Statements

For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias-Müller,2019] asks whether a certain natural propositional encoding of the above statement is ... more >>>

TR20-037 | 18th March 2020
Michal Garlik

Failure of Feasible Disjunction Property for $k$-DNF Resolution and NP-hardness of Automating It

We show that for every integer $k \geq 2$, the Res($k$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and Müller [FOCS, 2019] to Res($k$). We show that if NP is not included in P (resp. QP, SUBEXP) then ... more >>>

TR21-138 | 23rd September 2021
Rahul Santhanam, Iddo Tzameret

Iterated Lower Bound Formulas: A Diagonalization-Based Approach to Proof Complexity

We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

We give an explicit sequence of CNF formulas $\{\phi_n\}$ such that VNP$\neq$VP iff there are ... more >>>

ISSN 1433-8092 | Imprint