| 1. |
- Austrin, Per, 1981-, et al.
(författare)
-
Perfect Matching in Random Graphs is as Hard as Tseitin
- 2022
-
Ingår i: Proceedings of the 2022 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). - : Association for Computing Machinery (ACM). ; , s. 979-1012
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 2. |
- Austrin, Per, 1981-, et al.
(författare)
-
Sum-Of-Squares Lower Bounds for the Minimum Circuit Size Problem
- 2023
-
Ingår i: 38th Computational Complexity Conference, CCC 2023. - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
-
Konferensbidrag (refereegranskat)abstract
- We prove lower bounds for the Minimum Circuit Size Problem (MCSP) in the Sum-of-Squares (SoS) proof system. Our main result is that for every Boolean function f : (0, 1)n → (0, 1), SoS requires degree Ω(s1−ϵ) to prove that f does not have circuits of size s (for any s > poly(n)). As a corollary we obtain that there are no low degree SoS proofs of the statement NP ⊈ P/poly. We also show that for any 0 < α < 1 there are Boolean functions with circuit complexity larger than 2nα but SoS requires size 22Ω(nα) to prove this. In addition we prove analogous results on the minimum monotone circuit size for monotone Boolean slice functions. Our approach is quite general. Namely, we show that if a proof system Q has strong enough constraint satisfaction problem lower bounds that only depend on good expansion of the constraint-variable incidence graph and, furthermore, Q is expressive enough that variables can be substituted by local Boolean functions, then the MCSP problem is hard for Q.
|
|
| 3. |
- Conneryd, Jonas, et al.
(författare)
-
Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
- 2023
-
Ingår i: Proceedings - 2023 IEEE 64th Annual Symposium on Foundations of Computer Science, FOCS 2023. - 0272-5428. - 9798350318944 ; , s. 1-11
-
Konferensbidrag (refereegranskat)abstract
- We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse Erdős-Rényi random graphs, are 3-colourable.
|
|
| 4. |
- De Rezende, Susanna F., et al.
(författare)
-
Clique Is Hard on Average for Unary Sherali-Adams
- 2023
-
Ingår i: Proceedings - 2023 IEEE 64th Annual Symposium on Foundations of Computer Science, FOCS 2023. - 0272-5428. - 9798350318944 ; , s. 12-25
-
Konferensbidrag (refereegranskat)abstract
- We prove that unary Sherali-Adams requires proofs of size nΩ(d) to rule out the existence of an nΘ(1)-clique in Erdős-Rényi random graphs whose maximum clique is of size d ≤ 2 log n. This lower bound is tight up to the multiplicative constant in the exponent. We obtain this result by introducing a technique inspired by pseudo-calibration which may be of independent interest. The technique involves defining a measure on monomials that precisely captures the contribution of a monomial to a refutation. This measure intuitively captures progress and should have further applications in proof complexity.
|
|
| 5. |
- de Rezende, Susanna F., et al.
(författare)
-
Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
- 2020
-
Ingår i: CCC '20: Proceedings of the 35th Computational Complexity Conference 2020. - : Schloss Dagstuhl–Leibniz-Zentrum für Informatik. - 1868-8969. - 9783959771566 ; 169, s. 28-1
-
Konferensbidrag (refereegranskat)abstract
- We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson'01] and highly unbalanced, dense graphs as in [Raz'04] and [Razborov'03,'04]. We obtain our results by revisiting Razborov's pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.
|
|
| 6. |
- Risse, Kilian, 1991-, et al.
(författare)
-
On bounded depth proofs for Tseitin formulas on the grid; revisited
- 2022
-
Ingår i: 2022 IEEE 63RD ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE (FOCS). - : Institute of Electrical and Electronics Engineers (IEEE). ; , s. 1138-1149
-
Konferensbidrag (refereegranskat)abstract
- 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))).
|
|
| 7. |
- Risse, Kilian, 1991-
(författare)
-
On Long Proofs of Simple Truths
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 8. |
|
|
