Tuomas Hakoniemi defended his PhD thesis Size bounds for algebraic and semialgebraic proof systems on March 03, 2022. The thesis was produced within the UPC doctoral program on Computing and his advisor was Albert Atserias. Currently, he is a postdoctoral researcher at Imperial College London in the Iddo Tzameret group.
Thesis summary
Proof complexity is a field in the crossroads of mathematical logic and computational complexity theory that studies the resources needed to prove formal statements in different logical calculi. In 1979, Cook and Reckhow proposed a general definition of a propositional proof system as a poly-time computable function onto the set of tautologies. With this definition at hand they made the simple but foundational observation that there is no propositional proof system for classical propositional logic that has short, i.e. polynomial-sized, proofs for all tautologies unless NP is closed under complementation.
Besides logic, different proof calculi can be found also in other parts of mathematics. In this thesis we study calculi arising from algebraic geometry and combinatorial optimization. We consider the proof complexity of algebraic and semialgebraic proof systems Polynomial Calculus, Sums-of-Squares and Sherali-Adams. These systems are refutation systems for unsatisfiable sets of polynomial constraints. Polynomial Calculus, introduced by Clegg, Edmonds and Impagliazzo, has its roots in the theory of Gröbner bases in computational algebraic geometry, while Sums-of-Squares and Sherali-Adams proof systems stem from the hierarchies of semidefinite and linear relaxations in polynomial optimization introduced by Lasserre, and Sherali and Adams, respectively.
The most studied complexity measure for these systems is the degree of the proofs, not least due to the close connections to the levels in the hierarchies mentioned above. This thesis concentrates, however, on other possible complexity measures of interest to proof complexity, monomial-size and bit-complexity, i.e. the number of (distinct) monomials needed in the proofs and the number of bits needed to represent the proofs (over rationals) in binary notation. We aim to showcase that there is a reasonably well-behaved theory for these measures also.
Firstly we tie the complexity measures of degree and monomial-size together by proving size-degree trade-offs for Sums-of-Squares and Sherali-Adams. In more detail, we show that if there is a refutation with at most s many monomials, then there is a refutation of degree O(√(n log s) + k), where k is the maximum degree of the constraints and n is the number of variables. This gives us a criterion for monomial-size lower bounds from degree lower bounds. These results are analogous to the celebrated size-width trade-off for Resolution of Ben-Sasson and Wigderson. For Polynomial Calculus similar trade-off was obtained earlier by Impagliazzo, Pudlák and Sgall.
Secondly we prove a form of feasible interpolation for all three systems. Feasible interpolation is a framework introduced by Krajícek for reducing lower bounds in proof complexity to lower bounds in other computational models. The basic form of feasible interpolation takes a refutation of two formulas φ(x, z) and ψ(y, z) with disjoint sequences x, y and z of variables, and extracts from it a somehow feasible algorithm computing an interpolant of the formulas, i.e. an algorithm that given an assignment a to the z-variables decides whether φ(x, a) or ψ(y, a) is unsatisfiable. We show that for each of the three systems there is a polynomial time algorithm that given a refutation of two mutually unsatisfiable sets P(x, z) and Q(y, z) of polynomial constraints and an assignment a finds a refutation of either P(x, a) or Q(y, a).
Finally we consider the relationship between monomial size and bit-complexity in Polynomial Calculus and Sums-of-Squares. We exhibit an unsatisfiable set of polynomial constraints that has both Polynomial Calculus and Sums-of-Squares refutations with only polynomially many distinct monomials, but for which any Polynomial Calculus or Sums-of-Squares refutation requires exponential bit-complexity.
Besides the emphasis on complexity measures other than degree, another unifying theme in all the three results is the use of semantic characterizations of resource-bounded proofs and refutations. All results make heavy use of the completeness properties of such characterizations: we argue for the existence of resource-bounded proofs and refutations from the non-existence of suitable semantic objects, and for the existence of the semantic objects from the non-existence of resourceb-ounded proofs or refutations. All in all, the work on these semantic characterizations presents itself as the fourth central contribution of this thesis.
Highlighted publication: Albert Atserias and Tuomas Hakoniemi. Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs. In Proceedings of the 34th Computational Complexity Conference (CCC 2019), Leibniz International Proceedings in Informatics (LIPIcs) 137 (2019), pages 24:1–24:20. Published by Schloss Dagstuhl–Leibniz-Zentrum für Informatik, edited by Amir Shpilka.