The semantics of decision problems are always essentially independent of the
underlying representation. Thus the space of input data (under appropriate
indexing) is closed
under action of the symmetrical group $S_n$ (for a specific data-size)
and the input-output relation is closed under the action of $S_n$.
more >>>

Proof complexity, the study of the lengths of proofs in
propositional logic, is an area of study that is fundamentally connected
both to major open questions of computational complexity theory and
to practical properties of automated theorem provers. In the last
decade, there have been a number of significant advances ... 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 ... 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 ... more >>>

We study the complexity of proving the Pigeon Hole
Principle (PHP) in a monotone variant of the Gentzen Calculus, also
known as Geometric Logic. We show that the standard encoding
of the PHP as a monotone sequent admits quasipolynomial-size proofs
in this system. This result is a consequence of ... 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 >>>

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

We prove a quasi-polynomial lower bound on the size of bounded-depth
Frege proofs of the pigeonhole principle $PHP^{m}_n$ where
$m= (1+1/{\polylog n})n$.
This lower bound qualitatively matches the known quasi-polynomial-size
bounded-depth Frege proofs for these principles.
Our technique, which uses a switching lemma argument like other lower bounds
for ... more >>>

We present a simple proof of the bounded-depth Frege lower bounds of
Pitassi et. al. and Krajicek et. al. for the pigeonhole
principle. Our method uses the interpretation of proofs as two player
games given by Pudlak and Buss. Our lower bound is conceptually
simpler than previous ones, and relies ... 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 >>>

We define a collection of Prover-Delayer games that characterize certain subsystems of resolution. This allows us to give some natural criteria which guarantee lower bounds on the resolution width of a formula, and to extend these results to formulas of unbounded initial width.

We also use games to give upper ... more >>>

We prove that an \omega(log^3 n) lower bound for the three-party number-on-the-forehead (NOF) communication complexity of the set-disjointness function implies an n^\omega(1) size lower bound for tree-like Lovasz-Schrijver systems that refute unsatisfiable CNFs. More generally, we prove that an n^\Omega(1) lower bound for the (k+1)-party NOF communication complexity of set-disjointness ... 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 that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following:

1. Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial ... more >>>

Let $\phi$ be a 3CNF formula with n variables and m clauses. A
simple nonconstructive argument shows that when m is
sufficiently large compared to n, most 3CNF formulas are not
satisfiable. It is an open question whether there is an efficient
refutation algorithm that for most such formulas proves ... more >>>

The importance of {\em width} as a resource in resolution theorem proving
has been emphasized in work of Ben-Sasson and Wigderson. Their results show that lower
bounds on the size of resolution refutations can be proved in a uniform manner by
demonstrating lower bounds on the width ... more >>>

We consider extensions of the DPLL approach to satisfiability testing that add a version of memoization, in which formulas that the algorithm has previously shown to be unsatisfiable are remembered for later use. Such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability. We formalize these methods by ... more >>>

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

We demonstrate a family of propositional formulas in conjunctive normal form
so that a formula of size $N$ requires size $2^{\Omega(\sqrt[7]{N/logN})}$
to refute using the tree-like OBDD refutation system of
Atserias, Kolaitis and Vardi
with respect to all variable orderings.
All known symbolic quantifier elimination algorithms for satisfiability
generate ... 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 disjointness requires randomized communication
Omega(\frac{n^{1/2k}}{(k-1)2^{k-1}2^{2^{k-1}}})
in the general k-party number-on-the-forehead model of complexity.
The previous best lower bound was Omega(\frac{log n}{k-1}). By
results of Beame, Pitassi, and Segerlind, this implies
2^{n^{Omega(1)}} lower bounds on the size of tree-like Lovasz-Schrijver
proof systems needed to refute certain unsatisfiable ... more >>>

The planar Hajos calculus is the Hajos calculus with the restriction that all the graphs that appear in the construction (including a final graph) must be planar. We prove that the planar Hajos calculus is polynomially bounded iff the HajLos calculus is polynomially bounded.

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

The k-DNF resolution proof systems are a family of systems indexed by
the integer k, where the kth member is restricted to operating with
formulas in disjunctive normal form with all terms of bounded arity k
(k-DNF formulas). This family was introduced in [Krajicek 2001] as an
extension of the ... more >>>

We present a generic method for converting any family of unsatisfiable CNF formulas that require large resolution rank into CNF formulas whose refutation requires large rank for proof systems that manipulate polynomials or polynomial threshold functions of degree at most $k$ (known as ${\rm Th}(k)$ proofs). Such systems include: Lovasz-Schrijver ... 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&ouml;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 >>>

Let $g$ be a map defined as the Nisan-Wigderson generator
but based on an $NP \cap coNP$-function $f$. Any string $b$ outside the range of
$g$ determines a propositional tautology $\tau(g)_b$ expressing this
fact. Razborov \cite{Raz03} has conjectured that if $f$ is hard on average for
P/poly then these ... more >>>

Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles.
We broadly investigate Parameterized Resolution obtaining the following ... more >>>

This paper shows that the use of ``local symmetry breaking'' can dramatically reduce the length of propositional refutations. For each of the three propositional proof systems known as (i) treelike resolution, (ii) resolution, and (iii) k-DNF resolution, we describe families of unsatisfiable formulas in conjunctive normal form (CNF) that are ... more >>>

In this note we show that the asymmetric Prover-Delayer game developed by Beyersdorff, Galesi, and Lauria (ECCC TR10-059) for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover-Delayer game to show a lower bound of the form $2^{\Omega(n\log n)}$ for the pigeonhole ... more >>>

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege--yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analogue of Frege proofs, different from that given in Buss ... 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. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There ... more >>>

A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that framework the parameterized version of any proof system is not fpt-bounded for some technical reasons, but we remark that this question becomes much more interesting if we restrict ourselves to those parameterized contradictions ... more >>>

Separating different propositional proof systems---that is, demonstrating that one proof system cannot efficiently simulate another proof system---is one of the main goals of proof complexity. Nevertheless, all known separation results between non-abstract proof systems are for specific families of hard tautologies: for what we know, in the average case all ... more >>>

We give the first time-space tradeoff lower bounds for Resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size $N$ that have Resolution refutations of space and size each roughly $N^{\log_2 N}$ (and like all formulas have Resolution refutations of space $N$) for ... more >>>

We study arithmetic proof systems $\mathbb{P}_c(\mathbb{F})$ and $\mathbb{P}_f(\mathbb{F})$ operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field $\mathbb{F}$. We establish a series of structural theorems about these proof systems, the main one stating that $\mathbb{P}_c(\mathbb{F})$ proofs can be balanced: if a polynomial identity of ... more >>>