Till innehåll på sidan

On Long Proofs of Simple Truths

Tid: To 2022-10-27 kl 14.00

Plats: F3, Lindstedtsvägen 26 & 28, Stockholm

Videolänk: https://kth-se.zoom.us/j/68576785278

Språk: Engelska

Ämnesområde: Datalogi

Respondent: Kilian Risse , Teoretisk datalogi, TCS

Opponent: Associate Professor Benjamin Rossman, Duke University, Levine Science Research Center, Durham, NC, USA

Handledare: Per Austrin, Teoretisk datalogi, TCS; Johan Håstad, Matematik (Avd.); Jakob Nordström, Teoretisk datalogi, TCS

Exportera till kalender

QC 20221005

Abstract

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.

urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-319644