Maria Luisa Bonet, Juan Luis Esteban, Jan Johannsen

We prove an exponential lower bound for tree-like Cutting Planes

refutations of a set of clauses which has polynomial size resolution

refutations. This implies an exponential separation between tree-like

and dag-like proofs for both Cutting Planes and resolution; in both

cases only superpolynomial separations were known before.

In order to ...
more >>>

Michael Alekhnovich, Jan Johannsen, Alasdair Urquhart

This paper gives two distinct proofs of an exponential separation

between regular resolution and unrestricted resolution.

The previous best known separation between these systems was

quasi-polynomial.

Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov

We show that the size of any regular resolution refutation of Tseitin formula $T(G,c)$ based on a graph $G$ is at least $2^{\Omega(tw(G)/\log n)}$, where $n$ is the number of vertices in $G$ and $tw(G)$ is the treewidth of $G$. For constant degree graphs there is known upper bound $2^{O(tw(G))}$ ... more >>>

Zoë Bell

We show that is hard to find regular or even ordered (also known as Davis-Putnam) Resolution proofs, extending the breakthrough result for general Resolution from Atserias and Müller to these restricted forms. Namely, regular and ordered Resolution are automatable if and only if P = NP. Specifically, for a CNF ... more >>>

Klim Efremenko, Michal Garlik, Dmitry Itsykson

The proof system resolution over parities (Res($\oplus$)) operates with disjunctions of linear equations (linear clauses) over $\mathbb{F}_2$; it extends the resolution proof system by incorporating linear algebra over $\mathbb{F}_2$. Over the years, several exponential lower bounds on the size of tree-like Res($\oplus$) refutations have been established. However, proving a superpolynomial ... more >>>

Sam Buss, Emre Yolcu

Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with ... more >>>

Yaroslav Alekseev, Dmitry Itsykson

The propositional proof system resolution over parities (Res($\oplus$)) combines resolution and the linear algebra over GF(2). It is a challenging open question to prove a superpolynomial lower bound on the proof size in this system. For many years, superpolynomial lower bounds were known only in tree-like cases. Recently, Efremenko, Garlik, ... more >>>