Search for: All records

A major open problem in proof complexity is to prove superpolynomial lower bounds for AC0[p]-Frege proofs. This system is the analog of AC0 [p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years ([28, 30]), there are no significant lower bounds for AC0 [p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC0[p]-Frege, including Nullstellensatz ([3]), Polynomial Calculus ([9]), and SOS ([14]). However to date there has been no progress on AC0 [p]-Frege lower bounds. In this paper we study constant-depth extensions of the Polynomial Calculus [13]. We show that these extensions are much more powerful than was previously known. Our main result is that small depth (≤ 43) Polynomial Calculus (over a sufficiently large field) can polynomially effectively simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams, Sum-of-Squares (SOS), and Positivstellensatz Calculus (Dynamic SOS). Additionally, they can also quasi-polynomially effectively simulate AC0[q]-Frege for any prime q independent of the characteristic of the underlying field. They can also effectively simulate TC0-Frege if the depth is allowed to grow proportionally. Thus, proving strong lower bounds for constant-depth extensions of Polynomial Calculus would not only give lower bounds for AC0 [p]-Frege, but also for systems as strong as TC0-Frege. 

We show that Cutting Planes (CP) proofs are hard to find: Given an unsatisfiable formula F, It is -hard to find a CP refutation of F in time polynomial in the length of the shortest such refutation; and unless Gap-Hitting-Set admits a nontrivial algorithm, one cannot find a tree-like CP refutation of F in time polynomial in the length of the shortest such refutation. The first result extends the recent breakthrough of Atserias and M'uller (FOCS 2019) that established an analogous result for Resolution. Our proofs rely on two new lifting theorems: (1) Dag-like lifting for gadgets with many output bits. (2) Tree-like lifting that simulates an r-round protocol with gadgets of query complexity O(r). 

Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical understanding of whether restarts are indeed crucial to the power of CDCL solvers is missing. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a drunk randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection. 

One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., P 6⊆ NC1). Karchmer, Raz, and Wigderson [KRW95] suggested to approach this problem by proving that depth complexity behaves “as expected” with respect to the composition of functions f ⋄ g. They showed that the validity of this conjecture would imply that P 6⊆ NC^1 . Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function f, but only for few inner functions g. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the monotone version of the KRW conjecture. We prove it for every monotone inner function g whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the s-t-connectivity, clique, and generation functions. In order to carry this progress back to the non-monotone setting, we introduce a new notion of semi-monotone composition, which combines the non-monotone complexity of the outer function f with the monotone complexity of the inner function g. In this setting, we prove the KRW conjecture for a similar selection of inner functions g, but only for a specific choice of the outer function f. 

We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula F, it is NP-hard to find a refutation of F in the Nullstellensatz, Polynomial Calculus, or Sherali--Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Muller (FOCS 2019) that established an analogous result for Resolution. 

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems: • We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. • We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal. 

We prove that the P^NP-type query complexity (alternatively, decision list width) of any boolean function f is quadratically related to the P^NP-type communication complexity of a lifted version of f. As an application, we show that a certain "product" lower bound method of Impagliazzo and Williams (CCC 2010) fails to capture P^NP communication complexity up to polynomial factors, which answers a question of Papakonstantinou, Scheder, and Song (CCC 2014).