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 constantdepth 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 wellstudied semialgebraic proof systems: Cutting Planes, SheraliAdams, SumofSquares (SOS), and Positivstellensatz Calculus (Dynamic SOS). Additionally, they can also quasipolynomially effectively simulate AC0[q]Frege for any prime q independent of the characteristic of the underlying field. They can also effectively simulate TC0Frege if the depth is allowed to grow proportionally. Thus, proving strong lower bounds for constantdepth extensions of Polynomial Calculus would not only give lower bounds for AC0 [p]Frege, but also for systems as strong as TC0Frege.
more »
« less
Stabbing Planes
We develop a new semialgebraic proof system called Stabbing Planes which formalizes modern branchandcut algorithms for integer programming and is in the style of DPLLbased modern SAT solvers. As with DPLL there is only a single rule: the current polytope can be subdivided by branching on an inequality and its “integer negation.” That is, we can (nondeterministically choose) a hyperplane ax ≥ b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying ax ≥ b, the points satisfying ax ≤ b, and the middle slab b − 1 < ax < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomialtime checkable. Among our results, we show that Stabbing Planes can efficiently simulate the Cutting Planes proof system, and is equivalent to a treelike variant of the R(CP) system of Krajicek [54]. As well, we show that it possesses short proofs of the canonical family of systems of F_2linear equations known as the Tseitin formulas. Finally, we prove linear lower bounds on the rank of Stabbing Planes refutations by adapting lower bounds in communication complexity and use these bounds in order to show that Stabbing Planes proofs cannot be balanced.
more »
« less
 NSFPAR ID:
 10343001
 Date Published:
 Journal Name:
 ArXivorg
 Volume:
 arxiv:2017
 Issue:
 arxiv:1710.03219v2
 ISSN:
 23318422
 Page Range / eLocation ID:
 129
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this


Dubois, Catherine ; Kerber, Manfred (Ed.)Solving a sparse linear system of the form Ax = b is a common engineering task, e.g., as a step in approximating solutions of differential equations. Inverting a large matrix A is often too expensive, and instead engineers rely on iterative methods, which progressively approximate the solution x of the linear system in several iterations, where each iteration is a much less expensive (sparse) matrixvector multiplication. We present a formal proof in the Coq proof assistant of the correctness, accuracy and convergence of one prominent iterative method, the Jacobi iteration. The accuracy and convergence properties of Jacobi iteration are wellstudied, but most past analyses were performed in real arithmetic; instead, we study those properties, and prove our results, in floatingpoint arithmetic. We then show that our results are properly reflected in a concrete implementation in the C language. Finally, we show that the iteration will not overflow, under assumptions that we make explicit. Notably, our proofs are faithful to the details of the implementation, including C program semantics and floatingpoint arithmetic.more » « less

Dubois, Catherine ; Kerber, Manfred (Ed.)Solving a sparse linear system of the form Ax = b is a common engineering task, e.g., as a step in approximating solutions of differential equations. Inverting a large matrix A is often too expensive, and instead engineers rely on iterative methods, which progressively approximate the solution x of the linear system in several iterations, where each iteration is a much less expensive (sparse) matrixvector multiplication. We present a formal proof in the Coq proof assistant of the correctness, accuracy and convergence of one prominent iterative method, the Jacobi iteration. The accuracy and convergence properties of Jacobi iteration are wellstudied, but most past analyses were performed in real arithmetic; instead, we study those properties, and prove our results, in floatingpoint arithmetic. We then show that our results are properly reflected in a concrete implementation in the C language. Finally, we show that the iteration will not overflow, under assumptions that we make explicit. Notably, our proofs are faithful to the details of the implementation, including C program semantics and floatingpoint arithmetic.more » « less

We explore algorithms and limitations for sparse optimization problems such as sparse linear regression and robust linear regression. The goal of the sparse linear regression problem is to identify a small number of key features, while the goal of the robust linear regression problem is to identify a small number of erroneous measurements. Specifically, the sparse linear regression problem seeks a ksparse vector x ∈ Rd to minimize ‖Ax − b‖2, given an input matrix A ∈ Rn×d and a target vector b ∈ Rn, while the robust linear regression problem seeks a set S that ignores at most k rows and a vector x to minimize ‖(Ax − b)S ‖2. We first show bicriteria, NPhardness of approximation for robust regression building on the work of [OWZ15] which implies a similar result for sparse regression. We further show finegrained hardness of robust regression through a reduction from the minimumweight kclique conjecture. On the positive side, we give an algorithm for robust regression that achieves arbitrarily accurate additive error and uses runtime that closely matches the lower bound from the finegrained hardness result, as well as an algorithm for sparse regression with similar runtime. Both our upper and lower bounds rely on a general reduction from robust linear regression to sparse regression that we introduce. Our algorithms, inspired by the 3SUM problem, use approximate nearest neighbor data structures and may be of independent interest for solving sparse optimization problems. For instance, we demonstrate that our techniques can also be used for the wellstudied sparse PCA problem.more » « less

Raz, Ran (Ed.)We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially all of the subsystems considered in this paper can simulate the wellstudied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity). Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it. These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proofcomplexity ones, especially the "feasible interpolation" technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems. Our first method is a functional lower bound, a notion of Grigoriev and Razborov, which is a function f' from nbit strings to a field, such that any polynomial f agreeing with f' on the boolean cube requires large algebraic circuit complexity. We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth3 powering formulas, readonce algebraic branching programs and multilinear formulas) where f'(x) equals 1/p(x) for a constantdegree polynomial p depending on the relevant circuit class. We believe these lower bounds are of independent interest in algebraic complexity, and show that they also imply lower bounds for the size of the corresponding IPS refutations for proving that the relevant polynomial p is nonzero over the boolean cube. In particular, we show superpolynomial lower bounds for refuting variants of the subsetsum axioms in these IPS subsystems. Our second method is to give lower bounds for multiples, that is, to give explicit polynomials whose all (nonzero) multiples require large algebraic circuit complexity. By extending known techniques, we give lower bounds for multiples for various restricted circuit classes such sparse polynomials, sums of powers of lowdegree polynomials, and roABPs. These results are of independent interest, as we argue that lower bounds for multiples is the correct notion for instantiating the algebraic hardness versus randomness paradigm of Kabanets and Impagliazzo. Further, we show how such lower bounds for multiples extend to lower bounds for refutations in the corresponding IPS subsystem.more » « less