| 1. |
- Alwen, Joël, et al.
(författare)
-
Cumulative Space in Black-White Pebbling and Resolution
- 2017
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. - 9783959770293
-
Konferensbidrag (refereegranskat)abstract
- We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko 2015] as a tool for obtaining results in cryptography. We consider instead the nondeterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10-15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström 2008, 2011], we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.
|
|
| 2. |
- Atserias, Albert, et al.
(författare)
-
Clique Is Hard on Average for Regular Resolution
- 2018
-
Ingår i: STOC'18. - New York, NY, USA : ASSOC COMPUTING MACHINERY. ; , s. 866-877
-
Konferensbidrag (refereegranskat)abstract
- We prove that for k << (4)root n regular resolution requires length n(Omega(k)) to establish that an Erdos Renyi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional n(Omega(k)) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.
|
|
| 3. |
- Atserias, Albert, et al.
(författare)
-
Clique Is Hard on Average for Regular Resolution
- 2021
-
Ingår i: Journal of the ACM. - : Association for Computing Machinery (ACM). - 0004-5411 .- 1557-735X. ; 68:4, s. 1-26
-
Tidskriftsartikel (refereegranskat)abstract
- We prove that for k ≫; 4√n regular resolution requires length nω(k) to establish that an ErdÅ's-Rényi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent and also implies unconditional nω(k) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.
|
|
| 4. |
- 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.
|
|
| 5. |
- De Rezende, Susanna F., et al.
(författare)
-
Automating algebraic proof systems is NP-hard
- 2021
-
Ingår i: STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. - New York, NY, USA : ACM. - 0737-8017. - 9781450380539 ; , s. 209-222
-
Konferensbidrag (refereegranskat)abstract
- We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula F, it is NP-hard to find a refutation of F in the Nullstellensatz, Polynomial Calculus, or Sherali-Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Müller (JACM 2020) that established an analogous result for Resolution.
|
|
| 6. |
- 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.
|
|
| 7. |
- 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.
|
|
| 8. |
- de Rezende, Susanna F., et al.
(författare)
-
How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)
- 2016
-
Ingår i: 2016 IEEE 57th Annual Symposium on Foundations of Computer Science (FOCS). - : IEEE Computer Society. - 9781509039333 ; , s. 295-304
-
Konferensbidrag (refereegranskat)abstract
- We obtain the first true size-space trade-offs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constant-size coefficients, and the lower bounds apply to length and formula space (i.e., number of inequalities in memory) even for derivations with exponentially large coefficients. These are also the first trade-offs to hold uniformly for resolution, polynomial calculus and cutting planes, thus capturing the main methods of reasoning used in current state-of-the-art SAT solvers. We prove our results by a reduction to communication lower bounds in a round-efficient version of the real communication model of [Krajicek ' 98], drawing on and extending techniques in [Raz and McKenzie ' 99] and [Goos et al. '15]. The communication lower bounds are in turn established by a reduction to trade-offs between cost and number of rounds in the game of [Dymond and Tompa '85] played on directed acyclic graphs. As a by-product of the techniques developed to show these proof complexity trade-off results, we also obtain an exponential separation between monotone-AC(i-1) and monotone-AC(i), improving exponentially over the superpolynomial separation in [Raz and McKenzie ' 99]. That is, we give an explicit Boolean function that can be computed by monotone Boolean circuits of depth log(i) n and polynomial size, but for which circuits of depth O (log(i-1) n) require exponential size.
|
|
| 9. |
- De Rezende, Susanna F., et al.
(författare)
-
KRW composition theorems via lifting
- 2020
-
Ingår i: Proceedings - 2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020. - 0272-5428. - 9781728196213 - 9781728196220 ; 2020-November, s. 43-49
-
Konferensbidrag (refereegranskat)abstract
- One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., mathrm{P} nsubseteq text{NC}{1}). Karchmer, Raz, and Wigderson [13] suggested to approach this problem by proving that depth complexity behaves'as expected' with respect to the composition of functions f diamond g. They showed that the validity of this conjecture would imply that mathrm{P} nsubseteq text{NC}{1}. Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function, but only for few inner functions. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the monotone version of the KRW conjecture. We prove it for every monotone inner function whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the s-t-connectivity, clique, and generation functions. In order to carry this progress back to the non-monotone setting, we introduce a new notion of semi-monotone composition, which combines the non-monotone complexity of the outer function with the monotone complexity of the inner function. In this setting, we prove the KRW conjecture for a similar selection of inner functions, but only for a specific choice of the outer function f.
|
|
| 10. |
- de Rezende, Susanna F., 1989-, et al.
(författare)
-
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
-
Annan publikation (övrigt vetenskapligt/konstnärligt)abstract
- We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomialline space if coefficients are restricted to be of polynomial magnitude.We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.
|
|
