Jan Krajicek

We prove an exponential lower bound on the size of proofs

in the proof system operating with ordered binary decision diagrams

introduced by Atserias, Kolaitis and Vardi. In fact, the lower bound

applies to semantic derivations operating with sets defined by OBDDs.

We do not assume ...
more >>>

Ján Pich

We prove that the Nisan-Wigderson generators based on computationally hard functions and suitable matrices are hard for propositional proof systems that admit feasible interpolation.

more >>>Albert Atserias, Elitza Maneva

We associate a CNF-formula to every instance of the mean-payoff game problem in such a way that if the value of the game is non-negative the formula is satisfiable, and if the value of the game is negative the formula has a polynomial-size refutation in $\Sigma_2$-Frege (i.e.~DNF-resolution). This reduces mean-payoff ... more >>>

Iddo Tzameret

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), as a family of unsatisfiable propositional formulas for which refutations of small size in any propositional proof system that possesses the feasible interpolation property imply an efficient *deterministic* refutation algorithm for random 3SAT with ... more >>>

Pavel Hrubes

We show that the semantic cutting planes proof system has feasible interpolation via monotone real circuits. This gives an exponential lower bound on proof length in the system.

We also pose the following problem: can every multivariate non-decreasing function be expressed as a composition of non-decreasing functions in two ... more >>>

Leroy Chew, Judith Clymo

In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial-time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a ... more >>>