The matrix cuts of Lovász and Schrijver are methods for tightening linear relaxations of zero-one programs by the addition of new linear inequalities. We address the question of how many new inequalities are necessary to approximate certain combinatorial problems, and we solve certain instances of Boolean satisfiability. Our first result is a size/rank tradeoff for tree-like Lovász–Schrijver refutations, showing that any refutation that has small size also has small rank. This allows us to immediately derive exponential-size lower bounds for tree-like refutations of many unsatisfiable systems of inequalities where, prior to our work, only strong rank bounds were known. Unfortunately, we show that this tradeoff does not hold more generally for derivations of arbitrary inequalities. We give a very simple example showing that derivations can be very small but nonetheless require maximal rank. This rules out a generic argument for obtaining a size-based integrality gap from the corresponding rank-based integrality gap. Our second contribution is to show that a modified argument can often be used to prove size-based integrality gaps from rank-based integrality gaps. We apply this method to prove size-based integrality gaps for several prominent examples where, prior to our work, only rank-based integrality gaps were known. Our third contribution is to prove new separation results. Using our machinery for converting rank-based lower bounds and integrality gaps into size-based lower bounds, we show that tree-like $\mbox{LS}_+$ cannot polynomially simulate tree-like cutting planes, and that tree-like $\mbox{LS}_+$ cannot polynomially simulate resolution.

The matrix cuts of Lovász and Schrijver are methods for tightening linear relaxations of zero-one programs by the addition of new linear inequalities. We address the question of how many new inequalities are necessary to approximate certain combinatorial problems, and to solve certain instances of Boolean satisfiability. Our first result is a size/rank tradeoff for tree-like Lovász-Schrijver refutations, showing that any refutation that has small size also has small rank. This allows us to immediately derive exponential size lower bounds for tree-like refutations of many unsatisfiable systems of inequalities where prior to our work, only strong rank bounds were known. Unfortunately, we show that this tradeoff does not hold more generally for derivations of arbitrary inequalities. We give a very simple example showing that derivations can be very small but nonetheless require maximal rank. This rules out a generic argument for obtaining a size-based integrality gap from the corresponding rank-based integrality gap. Our second contribution is to show that a modified argument can often be used to prove size-based integrality gaps from rank-based integrality gaps. We apply this method to prove size-based integrality gaps for several prominant examples where prior to our work, only rank-based integrality gaps were known. Our third contribution is to prove new separation results. Using our machinery for converting rank-based lower bounds and integrality gaps into size-based lower bounds, we show that tree-like LS+ cannot polynomially simulate tree-like Cutting Planes, and that tree-like LS+ cannot polynomially simulate resolution. We conclude by examining size/rank tradeoffs beyond the LS systems. We show that for Shirali-Adams and Lasserre systems, size/rank tradeoffs continue to hold, even in the general (non-tree) case. A full version of this paper is available at the Electronic Colloquium on Computational Complexity [23].

We show that tree-like OBDD proofs of unsatisfiability require an exponential increase (s rarr 2sOmega(1)) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase (s rarr 22(logs)Omega(1)) in proof size to simulate Res (O(log n)). The "OBDD proof system" that we consider has lines that are ordered binary decision diagrams in the same variables as the input formula, and is allowed to combine two previously derived OBDDs by any sound inference rule. In particular, this system abstracts satisfiability algorithms based upon explicit construction of OBDDs and satisfiability algorithms based upon symbolic quantifier elimination.

We prove that an $\omega(\log^4 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 treelike Lovász–Schrijver systems that refute unsatisfiable formulas in conjunctive normal form (CNFs). More generally, we prove that an $n^{\Omega(1)}$ lower bound for the $(k+1)$-party NOF communication complexity of set disjointness implies a $2^{n^{\Omega(1)}}$ size lower bound for all treelike proof systems whose formulas are degree k polynomial inequalities.

We prove that two-party randomized communication complexity satisfies a strong direct product property, so long as the communication lower bound is proved by a “corruption” or “one-sided discrepancy” method over a rectangular distribution. We use this to prove new n Ω(1) lower bounds for 3-player number-on-the-forehead protocols in which the first player speaks once and then the other two players proceed arbitrarily. Using other techniques, we also establish an Ω(n 1/(k−1)/(k − 1)) lower bound for k-player randomized number-on-the-forehead protocols for the disjointness function in which all messages are broadcast simultaneously. A simple corollary of this is that general randomized number-on-the-forehead protocols require Ω(log n/(k − 1)) bits of communication to compute the disjointness function.

We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m . Central to this is a new definition of reducibility from propositional formulas to systems of polynomials. Using our definition of reducibility, most previously studied propositional formulas reduce to their polynomial translations. When combined with a previous result of the authors, this establishes the first size separation between Nullstellensatz and polynomial calculus refutations. We also obtain new upper bounds on refutation sizes for certain CNFs in constant-depth Frege with counting axioms systems.

We prove that corruption, one of the most powerful measures used to analyze 2-party randomized communication complexity, satisfies a strong direct sum property under rectangular distributions. This direct sum bound holds even when the error is allowed to be exponentially close to 1. We use this to analyze the complexity of the widely-studied set disjointness problem in the usual "number-on-the-forehead" (NOF) model of multiparty communication complexity.

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to formulas in disjunctive normal form (DNFs) with small terms. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k + 1. Our results for Res(k) are as follows:The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k) for $k \leq \sqrt{\log n / \log \log n } $. For each constant k, there exists a constant w > k so that random w-CNFs require exponential size to refute in Res(k). For each constant k, there are sets of clauses which have polynomial size Res(k + 1) refutations but which require exponential size Res(k) refutations.

A fruitful connection between algorithm design and proof complexity is the formalization of the DPLL approach to satisfiability testing in terms of tree-like resolution proofs. We consider extensions of the DPLL approach that add some version of memoization, remembering formulas the algorithm has previously shown unsatisfiable. Various versions of such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability (S. M. Majercik et al., 1998; F. Bacchus et al., 2003). We formalize this method, and characterize the strength of various versions in terms of proof systems. These proof systems seem to be both new and simple, and have a rich structure. We compare their strength to several studied proof systems: tree-like resolution, regular resolution, general resolution, and Res(k). We give both simulations and separations.

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to DNFs with small conjunctions. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k+1. Our results for Res(k) are: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k), for k /spl les/ /spl radic/(log n/ log log n). 2. For each constant k, there exists a constant w > k so that random w-CNFs require exponential size to refute in Res(k). 3. For each constant k, there are sets of clauses which have polynomial size Res(k+1) refutations, but which require exponential size Res(k) refutations.

We give a family of tautologies whose algebraic translations have constant-degree, polynomial size polynomial calculus refutations over Z/sub 2/, but which require superpolynomial size bounded-depth Frege proofs from Count/sub 2/ axioms. This gives a superpolynomial size separation of bounded-depth Frege plus mod 2 counting axioms from bounded-depth Frege plus parity gates. Combined with another result of the authors, it gives the first size (as opposed to degree) separation between the polynomial calculus and Nullstellensatz systems.