kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On Long Proofs of Simple Truths
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-6913-3341
2022 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Propositional proof complexity is the study of certificates of infeasibility. In this thesis we consider several proof systems with limited deductive ability and unconditionally show that they require long refutations of the feasibility of certain Boolean formulas. We show that the depth $d$ Frege proof system, restricted to linesize $M$, requires proofs of length at least $\exp\bigl(n/(\log M)^{O(d)}\bigr)$ to refute the Tseitin contradiction defined over the $n \times n$ grid graph, improving upon the recent result of Pitassi et al. [PRT21]. Along the way we also sharpen the lower bound of Håstad [Hås20] on the depth $d$ Frege refutation size for the same formula from exponential in $\tilde{\Omega}(n^{1/59d})$ to exponential in$\tilde{\Omega}(n^{1/(2d-1)})$. We also consider the perfect matching formula defined over a sparse random graph on an odd number of vertices $n$. We show that polynomial calculus over fields of characteristic $\neq 2$ and sum of squares require size exponential in $\Omega(n/\log^2 n)$ to refute said formula. For depth $d$ Frege we show that there is a constant $\delta > 0$ such that refutations of these formulas require size $\exp\bigl(\Omega(n^{\delta/d})\bigl)$. The perfect matching formula has a close sibling over bipartite graphs: the graph pigeonhole principle. There are two methods to prove resolution refutation size lower bounds for the pigeonhole principle. On the one hand there is the general width-size tradeoff by Ben-Sasson and Wigderson [BW01] which can be used to show resolution refutation size lower bounds in the setting where we have a sparse bipartite graph with $n$ holes and $m \ll n^2$pigeons. On the other hand there is the pseudo-width technique developed by Razborov [Raz04] that applies for any number of pigeons, but requires the graph to be somewhat dense. We extend the latter technique to also cover the previous setting and more: for example, it has been open whether the functional pigeonhole principle defined over a random bipartite graph of bounded degree and $\poly(n) \ge n^2$ pigeons requires super-polynomial size resolution refutations. We answer this and related questions. Finally we also study the circuit tautology which claims that a Boolean function has a circuit of size $s$ computing it. For $s = \poly(n)$ we prove an essentially optimal Sum of Squares degree lower bound of $\Omega(s^{1-\eps})$ to refute this claim for any Boolean function. Further, we show that for any $0 < \alpha < 1$ there are Boolean functions on $n$ bits with circuit complexity larger than$2^{n^\alpha}$ but the Sum of Squares proof system requires size $2^{\bigl(2^{\Omega(n^\alpha)}\bigr)}$ to prove this. Lastly we show that these lower bounds can also be extended to the monotone setting.

Abstract [sv]

Propositionell beviskomplexitet är studerar certifikat av icke-satisfierbarhet. Vi betraktar bevissystem med begränsad deduktivförmåga och bevisar ovillkorliga undre gränser för längden på vederläggningar av formlers satisferbarhet. Denna avhandling bevisar flera nya sådana undre gränser för bevissystemen resolution, polynomialkalkyl, kvadratsummor, och Frege-system av begränsat djup. Vi visar att Frege-systemet av djup $d$, begränsat till rader av storlek $M$, kräver minst bevis av längd minst $\exp\bigl(n/(\log M)^{O(d)}\bigr)$ för att motbevisa Tseitin-kontradiktionen definierad över $n \times n$-rutnätet, vilket förbättrar ett nyligen visat resultat av Pitassi et al. [PRT21]. Längs vägen skärper vi även Håstads undre gräns [Hås20] för längd för Frege av djup $d$ för samma formel från exponentiell i $\tilde{\Omega}(n^{1/59d})$ till exponentiell i $\tilde{\Omega}(n^{1/(2d-1)})$. Vi betraktar också formeln för perfekt matchning över en gles slumpgraf med ett udda antal hörn $n$. Vi visar att polynomkalkyl över kroppar med karaktäristik $\ne 2$ och kvadratsummor kräver längd exponentiell i $\Omega(n/\log^2 n)$ för att motbevisa denna formel. För Frege av djup $d$ visar vi att det finns en konstant $\delta > 0$ så att vederläggningar av dessa formler kräver storlek $\exp\bigl(\Omega(n^{\delta/d})\bigl)$. Formeln för perfekt matchning har ett nära syskon över bipartitagrafer: duvslagsprincipen över grafer. Det finns två metoder för att visa undre gränser för refutations för duvslagsprincipen. Å ena sidan finns Ben-Sasson och Wigdersons [BW01] generella avvägning mellan bredd och storlek som kan användas för att visa undre gränser för resolution i fallet där vi har en gles bipartit graf med $n$ hål och $m \ll n^2$ duvor. Å andra sidan finns pseudo-bredd-tekniken utvecklad av Razborov[Raz04] som kan appliceras för valfritt antal duvor, men kräver att grafen är någorlunda tät. Vi utökar den senare tekniken till att även täcka det förstnämnda fallet och mer: till exempel har det varit öppet om den funktionella duvslagssprincipen definierad över en slumpmässig bipartit graf med begränsade gradtal och $\poly(n) \ge n^2$ duvor kräver motbevis av superpolynomisk storlek. Vi besvarar detta och relaterade frågor. Slutligen studerar vi också kretstautologin som hävdar att en Boolean funktion har en krets av storlek $s$ som beräknar den. Vi bevisar en väsentligen optimal undre gräns för gradtal för kvadratsummor på $\Omega(s^{1-\eps})$ för att motbevisa detta påstående för varje Boolesk funktion, för $s > \poly(n)$. Vidare visar vi att det för alla $0 < \alpha < 1$ finns Booleska funktioner på $n$ bitar med kretskomplexitet större än $2^{n^\alpha}$ men där kvadratsummor kräver storlek $2^{\bigl(2^{\Omega(n^\alpha)}\bigr)}$ för att bevisa detta.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2022. , p. x, 44
Series
TRITA-EECS-AVL ; 2022:55
Keywords [en]
Computational Complexity, Lower Bounds, Proof Complexity
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-319644ISBN: 978-91-8040-354-2 (print)OAI: oai:DiVA.org:kth-319644DiVA, id: diva2:1701114
Public defence
2022-10-27, https://kth-se.zoom.us/j/68576785278, F3, Lindstedtsvägen 26, Stockholm, 14:00 (English)
Opponent
Supervisors
Note

QC 20221005

Available from: 2022-10-05 Created: 2022-10-04 Last updated: 2022-10-10Bibliographically approved
List of papers
1. On bounded depth proofs for Tseitin formulas on the grid; revisited
Open this publication in new window or tab >>On bounded depth proofs for Tseitin formulas on the grid; revisited
2022 (English)In: 2022 IEEE 63RD ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE (FOCS), Institute of Electrical and Electronics Engineers (IEEE) , 2022, p. 1138-1149Conference paper, Published paper (Refereed)
Abstract [en]

We study Frege proofs using depth-d Boolean formulas for the Tseitin contradiction on n x n grids. We prove that if each line in the proof is of size M then the number of lines is exponential in n/(logM)(O(d)). This strengthens a recent result of Pitassi et al. [12]. The key technical step is a multi-switching lemma extending the switching lemma of Hastad [8] for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in (Omega) over tilde (n(1/59d)) to exponential in (Omega) over tilde (n(1/(2d-1))).

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Series
Annual IEEE Symposium on Foundations of Computer Science, ISSN 0272-5428
Keywords
proof complexity, bounded depth Frege
National Category
Discrete Mathematics
Identifiers
urn:nbn:se:kth:diva-319642 (URN)10.1109/FOCS54457.2022.00110 (DOI)000909382900104 ()2-s2.0-85146343295 (Scopus ID)
Conference
2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS), 31 October - 3 November 2022, Denver, CO, USA
Note

Part of proceedings: ISBN 978-166545519-0

QC 20221011

Available from: 2022-10-04 Created: 2022-10-04 Last updated: 2023-02-28Bibliographically approved
2. Perfect Matching in Random Graphs is as Hard as Tseitin
Open this publication in new window or tab >>Perfect Matching in Random Graphs is as Hard as Tseitin
2022 (English)In: Proceedings of the 2022 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), Association for Computing Machinery (ACM), 2022, p. 979-1012Conference paper, Published paper (Refereed)
Abstract [en]

We study the complexity of proving that a sparse random regular graph on an odd number of vertices does not have a perfect matching, and related problems involving each vertex being matched some pre-specified number of times. We show that this requires proofs of degree (n= log n) in the Polynomial Calculus (over fields of characteristic 6= 2) and Sum-of-Squares proof systems, and exponential size in the bounded-depth Frege proof system. This resolves a question by Razborov asking whether the Lovasz-Schrijver proof system requires nrounds to refute these formulas for some > 0. The results are obtained by a worst-case to averagecase reduction of these formulas relying on a topological embedding theorem which may be of independent interest.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2022
National Category
Discrete Mathematics
Identifiers
urn:nbn:se:kth:diva-318772 (URN)2-s2.0-85129087365 (Scopus ID)
Conference
33rd Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2022, Alexander, 9 January 2022, through 12 January 2022
Note

QC 20220928

Part of proceedings: ISBN 978-161197707-3

Available from: 2022-09-22 Created: 2022-09-22 Last updated: 2023-01-31Bibliographically approved
3. Sum-of-Squares Lower Bounds for the Minimum Circuit Size Problem
Open this publication in new window or tab >>Sum-of-Squares Lower Bounds for the Minimum Circuit Size Problem
(English)Manuscript (preprint) (Other academic)
National Category
Discrete Mathematics
Identifiers
urn:nbn:se:kth:diva-318776 (URN)
Note

QC 20221005

Available from: 2022-09-22 Created: 2022-09-22 Last updated: 2022-10-05Bibliographically approved
4. Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
Open this publication in new window or tab >>Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
2020 (English)In: 35th Computational Complexity Conference (CCC 2020), Schloss Dagstuhl–Leibniz-Zentrum für Informatik , 2020, Vol. 169, p. 28-1Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2020
Series
Leibniz International Proceedings in Informatics (LIPIcs)
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-282846 (URN)10.4230/LIPIcs.CCC.2020.28 (DOI)2-s2.0-85089398484 (Scopus ID)
Conference
Computational Complexity Conference (CCC 2020)
Available from: 2020-10-01 Created: 2020-10-01 Last updated: 2024-03-18Bibliographically approved

Open Access in DiVA

kappa(815 kB)264 downloads
File information
File name FULLTEXT01.pdfFile size 815 kBChecksum SHA-512
7e1a03b08b1516f9e0ddd5a7d9e9f7c2a15d18077828b4cc00bab52261171a6929b533e695d4a5365fbda2a4f1cce3f674f12d916f507fb895ca010a90c1233e
Type summaryMimetype application/pdf

Authority records

Risse, Kilian

Search in DiVA

By author/editor
Risse, Kilian
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 701 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf