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