In a semantic resolution proof we operate with clauses only but allow {\em arbitrary} rules of inference: C_1 C_2 ... C_m __________________ C Consistency is the only requirement. We prove a very simple exponential lower bound for the size of bounded fanin semantic resolution proofs of a general {\em Hitting ... more >>>

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

The width of a Resolution proof is defined to be the maximal number of literals in any clause of the proof. In this paper we relate proof width to proof length (=size), in both general Resolution, and its tree-like variant. The following consequences of these relations reveal width as a ... more >>>

We study space complexity in the framework of propositional proofs. We consider a natural model analogous to Turing machines with a read-only input tape, and such popular propositional proof systems as Resolution, Polynomial Calculus and Frege systems. We propose two different space measures, corresponding to the maximal number of bits, ... more >>>

We present the best known separation between tree-like and general resolution, improving on the recent $\exp(n^\epsilon)$ separation of \cite{BEGJ98}. This is done by constructing a natural family of contradictions, of size $n$, that have $O(n)$-size resolution refutations, but only $\exp (\Omega(n/\log n))$-size tree-like refutations. This result implies that the most ... more >>>

A basic property of minimally unsatisfiable clause-sets F is that c(F) >= n(F) + 1 holds, where c(F) is the number of clauses, and n(F) the number of variables. Let MUSAT(k) be the class of minimally unsatisfiable clause-sets F with c(F) <= n(F) + k. Poly-time decision algorithms are known ... more >>>

We call a pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ {\em hard} for a propositional proof system $P$ if $P$ can not efficiently prove the (properly encoded) statement $G_n(x_1,\ldots,x_n)\neq b$ for {\em any} string $b\in\{0,1\}^m$. We consider a variety of ``combinatorial'' pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and ... more >>>

We study the space complexity of refuting unsatisfiable random $k$-CNFs in the Resolution proof system. We prove that for any large enough $\Delta$, with high probability a random $k$-CNF over $n$ variables and $\Delta n$ clauses requires resolution clause space of $\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$, for any $0<\epsilon<1/2$. For constant $\Delta$, ... more >>>

Recently, Raz established exponential lower bounds on the size of resolution proofs of the weak pigeonhole principle. We give another proof of this result which leads to better numerical bounds. Specifically, we show that every resolution proof of $PHP^m_n$ must have size $\exp\of{\Omega(n/\log m)^{1/2}}$ which implies an $\exp\of{\Omega(n^{1/3})}$ bound when ... 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. more >>>

We prove exponential separations between the sizes of particular refutations in negative, respectively linear, resolution and general resolution. Only a superpolynomial separation between negative and general resolution was previously known. Our examples show that there is no strong relationship between the size and width of refutations in negative and linear ... more >>>

We show that every resolution proof of the {\em functional} version $FPHP^m_n$ of the pigeonhole principle (in which one pigeon may not split between several holes) must have size $\exp\of{\Omega\of{\frac n{(\log m)^2}}}$. This implies an $\exp\of{\Omega(n^{1/3})}$ bound when the number of pigeons $m$ is arbitrary. more >>>

We present the first example of a natural distribution on instances of an NP-complete problem, with the following properties. With high probability a random formula from this distribution (a) is unsatisfiable, (b) has a short proof that can be found easily, and (c) does not have a short (general) resolution ... more >>>

Having good algorithms to verify tautologies as efficiently as possible is of prime interest in different fields of computer science. In this paper we present an algorithm for finding Resolution refutations based on finding tree-like Res(k) refutations. The algorithm is based on the one of Beame and Pitassi \cite{BP96} for ... more >>>

Bayesian inference and counting satisfying assignments are important problems with numerous applications in probabilistic reasoning. In this paper, we show that plain old DPLL equipped with memoization can solve both of these problems with time complexity that is at least as good as all known algorithms. Furthermore, DPLL with memoization ... more >>>

We show that the Player-Adversary game from a paper by Pudlak and Impagliazzo played over CNF propositional formulas gives an exact characterization of the space needed in treelike resolution refutations. This characterization is purely combinatorial and independent of the notion of resolution. We use this characterization to give for the ... more >>>

We consider the resolution proof complexity of propositional formulas which encode random instances of graph $k$-colorability. We obtain a tradeoff between the graph density and the resolution proof complexity. For random graphs with linearly many edges we obtain linear-exponential lower bounds on the length of resolution refutations. For any $\epsilon>0$, ... more >>>

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously ... more >>>

We introduce an algebraic proof system Pcrk, which combines together {\em Polynomial Calculus} (Pc) and {\em $k$-DNF Resolution} (Resk). This is a natural generalization to Resk of the well-known {\em Polynomial Calculus with Resolution} (Pcr) system which combines together Pc and Resolution. We study the complexity of proofs in such ... more >>>

Satisfiability algorithms have become one of the most practical and successful approaches for solving a variety of real-world problems, including hardware verification, experimental design, planning and diagnosis problems. The main reason for the success is due to highly optimized algorithms for SAT based on resolution. The most successful of these ... more >>>

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. ... more >>>

We present a greatly simplified proof of the length-space trade-off result for resolution in Hertel and Pitassi (2007), and also prove a couple of other theorems in the same vein. We point out two important ingredients needed for our proofs to work, and discuss possible conclusions to be drawn regarding ... more >>>

We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The ``OBDD proof ... more >>>

Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field of proof complexity, the resources of time and memory correspond to the length ... more >>>

A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space. In this paper we resolve the question by answering ... more >>>

We discovered a serious error in one of our previous submissions to ECCC and wish to make sure that this mistake is publicly known. The main argument of the report TR06-133 is in error. The paper claims to prove the result of the title by reduction from the (Exists,k)-pebble game, ... more >>>

For current state-of-the-art satisfiability algorithms based on the DPLL procedure and clause learning, the two main bottlenecks are the amounts of time and memory used. Understanding time and memory consumption, and how they are related to one another, is therefore a question of considerable practical importance. In the field of ... more >>>

Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that any arbitrary OBDD Apply refutation of the pigeonhole formula has an exponential size: we prove that the size of one ... more >>>

In the context of proving lower bounds on proof space in $k$-DNF resolution, [Ben-Sasson and Nordström 2009] introduced the concept of minimally unsatisfiable sets of $k$-DNF formulas and proved that a minimally unsatisfiable $k$-DNF set with $m$ formulas can have at most $O((mk)^{k+1})$ variables. They also gave an example of ... more >>>

The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. The typical approach ... more >>>