Show simple item record

dc.contributorAtserias, Albert
dc.contributor.authorHakoniemi, Tuomas Antero
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.date.accessioned2022-04-28T18:32:26Z
dc.date.available2022-04-26T07:46:42Z
dc.date.issued2022-03-25
dc.identifier.citationHakoniemi, T.A. Size bounds for algebraic and semialgebraic proof systems. Tesi doctoral, UPC, Departament de Ciències de la Computació, 2022.
dc.identifier.urihttp://hdl.handle.net/2117/366561
dc.description.abstractThis thesis concerns the proof complexity of algebraic and semialgebraic proof systems Polynomial Calculus, Sums-of-Squares and Sherali-Adams. The most studied complexity measure for these systems is the degree of the proofs. This thesis concentrates on other possible complexity measures of interest to proof complexity, monomial-size and bit-complexity. 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 a size-degree trade-off for Sums-of-Squares and Sherali-Adams. We show that if there is a refutation with at most s many monomials, then there is a refutation whose degree is of order square root of n log s plus k, where k is the maximum degree of the constraints and n is the number of variables. For Polynomial Calculus similar trade-off was obtained earlier by Impagliazzo, Pudlák and Sgall. Secondly we prove a feasible interpolation property for all three systems. We show that for each system there is a polynomial time algorithm that given two sets P(x,z) and Q(y,z) of polynomial constraints in disjoint sequences x,y and z of variables, a refutation of the union of P(x,z) and Q(y,z), and an assignment a to the z-variables, finds either a refutation of P(x,a) or a refutation of Q(y,a). Finally we consider the relation between monomial-size and bit-complexity in Polynomial Calculus and Sums-of-Squares. We show that there is an unsatisfiable set of polynomial constraints that has both Polynomial Calculus and Sums-of-Squares refutations of polynomial monomial-size, 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. All in all, the work on these semantic characterizations presents itself as the fourth central contribution of this thesis.
dc.description.abstractAquesta tesi tracta de la complexitat de les proves en els sistemes de prova algebraics i semialgebraics Càlcul Polinomial (Polynomial Calculus), Sumes de Quadrats (Sums of Squares), i Sherali-Adams. La mesura de complexitat més estudiada per a aquests sistemes és el grau dels polinomis. Aquesta tesi se centra en altres possibles mesures de complexitat d'interès per a la complexitat de proves: el nombre de monomis i la longitud de representació en nombre de bits. Pretenem demostrar que aquestes mesures admeten una teoria comparable i complementària a la teoria del grau com a mesura de complexitat. En primer lloc, establim una relació entre les mesures de grau i de nombre de monomis demostrant una propietat d'intercanvi (trade-off) entre les dues mesures per als sistemes Sumes de Quadrats i Sherali-Adams. Demostrem que si hi ha una refutació amb com a màxim s monomis, aleshores hi ha una refutació el grau de la qual és d'ordre de l'arrel quadrada de n.log(s) més k, on k és el grau màxim de les restriccions i n és el nombre de variables. Per al Càlcul Polinomial, una propietat d'intercanvi similar va ser obtinguda per Impagliazzo, Pudlák i Sgall. En segon lloc, demostrem que els tres sistemes admeten la propietat d'interpolació eficient. Mostrem que, per a cadascun dels sistemes, hi ha un algorisme de temps polinomial que, donat dos conjunts P(x,z) i Q(y,z) de restriccions polinomials en successions disjuntes de variables x, y i z, donada una refutació de la unió de les restriccions de P(x,z) i Q(y,z), i donada una assignació per a les variables z, troba una refutació de P(x,a) o una refutació de Q(y,a). Finalment considerem la relació entre el nombre de monomis i la longitud de representació en bits per al Càlcul Polinomial i per a Sumes de Quadrats. Mostrem que hi ha un conjunt insatisfactible de restriccions polinomials que admet refutacions tant en Càlcul Polinomial com en Sumes de Quadrats amb un nombre polinòmic de monomis, però per a les quals qualsevol refutació en Càlcul Polinomial o en Sumes de Quadrats requereix complexitat en nombre de bits exponencial. A més de l'èmfasi en les mesures de complexitat diferents del grau, un altre tema unificador en els tres resultats és l'ús de certes caracteritzacions semàntiques de proves i refutacions limitades en recursos. Tots els resultats fan un ús clau de la propietat de completesa d'aquestes caracteritzacions. Amb tot, el treball sobre aquestes caracteritzacions semàntiques es presenta com la quarta aportació central d'aquesta tesi.
dc.format.extent137 p.
dc.language.isoeng
dc.publisherUniversitat Politècnica de Catalunya
dc.rightsL'accés als continguts d'aquesta tesi queda condicionat a l'acceptació de les condicions d'ús establertes per la següent llicència Creative Commons: http://creativecommons.org/licenses/by/4.0/
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/
dc.sourceTDX (Tesis Doctorals en Xarxa)
dc.subjectÀrees temàtiques de la UPC::Informàtica
dc.titleSize bounds for algebraic and semialgebraic proof systems
dc.typeDoctoral thesis
dc.rights.accessOpen Access
dc.description.versionPostprint (published version)
dc.audience.degreeDOCTORAT EN COMPUTACIÓ (Pla 2012)
dc.identifier.tdxhttp://hdl.handle.net/10803/674118


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record