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 >>>