| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- Atserias, Albert, et al.
(författare)
-
Narrow Proofs May Be Maximally Long
- 2016
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 17:3
-
Tidskriftsartikel (refereegranskat)abstract
- We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n(Omega(w)). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n(O(w)) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.
|
|
| 4. |
- Atserias, A., et al.
(författare)
-
Narrow proofs may be maximally long
- 2014
-
Ingår i: Proceedings of the Annual IEEE Conference on Computational Complexity. - 9781479936267 ; , s. 286-297
-
Konferensbidrag (refereegranskat)abstract
- We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nω(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size nO(ω) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.
|
|
| 5. |
- Beyersdorff, Olaf, et al.
(författare)
-
A characterization of tree-like Resolution size
- 2013
-
Ingår i: Information Processing Letters. - : Elsevier BV. - 0020-0190 .- 1872-6119. ; 113:18, s. 666-671
-
Tidskriftsartikel (refereegranskat)abstract
- We explain an asymmetric Prover-Delayer game which precisely characterizes proof size in tree-like Resolution. This game was previously described in a parameterized complexity context to show lower bounds for parameterized formulas (Beyersdorff et al. (2013) [2]) and for the classical pigeonhole principle (Beyersdorff et al. (2010) [1]). The main point of this note is to show that the asymmetric game in fact characterizes tree-like Resolution proof size, i.e. in principle our proof method allows to always achieve the optimal lower bounds. This is in contrast with previous techniques described in the literature. We also provide a very intuitive information-theoretic interpretation of the game.
|
|
| 6. |
- Beyersdorff, Olaf, et al.
(författare)
-
A Characterization of Tree-Like Resolution Size
- 2012
-
Ingår i: Electronic Colloquium on Computational Complexity (ECCC). - 1433-8092. ; :161
-
Tidskriftsartikel (refereegranskat)abstract
- We explain an asymmetric Prover-Delayer game which precisely characterizes proof size in tree-like Resolution. This game was previously described in a parameterized complexity context to show lower bounds for parameterized formulas [BGL11] and for the classical pigeonhole principle [BGL10]. The main point of this note is to show that the asymmetric game in fact characterizes tree-like Resolution proof size, i. e. in principle our proof method allows to always achieve the optimal lower bounds. This is in contrast with previous techniques described in the literature. We also provide a very intuitive information-theoretic interpretation of the game.
|
|
| 7. |
- Beyersdorff, Olaf, et al.
(författare)
-
Parameterized Bounded-Depth Frege Is not Optimal
- 2012
-
Ingår i: ACM Transactions on Computation Theory. - : Association for Computing Machinery (ACM). - 1942-3454 .- 1942-3462. ; 4:3, s. 7-
-
Tidskriftsartikel (refereegranskat)abstract
- A general framework for parameterized proof complexity was introduced by Dantchev et al. [2007]. There, the authors show important results on tree-like Parameterized Resolution-a parameterized version of classical Resolution-and their gap complexity theorem implies lower bounds for that system. The main result of this article significantly improves upon this by showing optimal lower bounds for a parameterized version of bounded-depth Frege. More precisely, we prove that the pigeonhole principle requires proofs of size n Ω(k) in parameterized bounded-depth Frege, and, as a special case, in dag-like Parameterized Resolution. This answers an open question posed in Dantchev et al. [2007]. In the opposite direction, we interpret a well-known technique for FPT algorithms as a DPLL procedure for Parameterized Resolution. Its generalization leads to a proof search algorithm for Parameterized Resolution that in particular shows that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNFs
|
|
| 8. |
- Beyersdorff, Olaf, et al.
(författare)
-
Parameterized Complexity of DPLL Search Procedures
- 2013
-
Ingår i: ACM Transactions on Computational Logic. - : Association for Computing Machinery (ACM). - 1529-3785 .- 1557-945X. ; 14:3, s. 20-
-
Tidskriftsartikel (refereegranskat)abstract
- We study the performance of DPLL algorithms on parameterized problems. In particular, we investigate how difficult it is to decide whether small solutions exist for satisfiability and other combinatorial problems. For this purpose we develop a Prover-Delayer game that models the running time of DPLL procedures and we establish an information-theoretic method to obtain lower bounds to the running time of parameterized DPLL procedures. We illustrate this technique by showing lower bounds to the parameterized pigeonhole principle and to the ordering principle. As our main application we study the DPLL procedure for the problem of deciding whether a graph has a small clique. We show that proving the absence of a k-clique requires n(Omega(k)) steps for a nontrivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked by Beyersdorff et al. [2012] of understanding the Resolution complexity of this family of formulas.
|
|
| 9. |
- Chan, S. M., et al.
(författare)
-
Hardness of Approximation in PSPACE and Separation Results for Pebble Games
- 2015
-
Ingår i: Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS. - : Institute of Electrical and Electronics Engineers (IEEE). - 9781467381918 ; , s. 466-485
-
Konferensbidrag (refereegranskat)abstract
- We consider the pebble game on DAGs with bounded fan-in introduced in [Paterson and Hewitt '70] and the reversible version of this game in [Bennett '89], and study the question of how hard it is to decide exactly or approximately the number of pebbles needed for a given DAG in these games. We prove that the problem of deciding whether s pebbles suffice to reversibly pebble a DAG G is PSPACE-complete, as was previously shown for the standard pebble game in [Gilbert, Lengauer and Tarjan '80]. Via two different graph product constructions we then strengthen these results to establish that both standard and reversible pebbling space are PSPACE-hard to approximate to within any additive constant. To the best of our knowledge, these are the first hardness of approximation results for pebble games in an unrestricted setting (even for polynomial time). Also, since [Chan '13] proved that reversible pebbling is equivalent to the games in [Dymond and Tompa '85] and [Raz and McKenzie '99], our results apply to the Dymond - Tompa and Raz - McKenzie games as well, and from the same paper it follows that resolution depth is PSPACE-hard to determine up to any additive constant. We also obtain a multiplicative logarithmic separation between reversible and standard pebbling space. This improves on the additive logarithmic separation previously known and could plausibly be tight, although we are not able to prove this. We leave as an interesting open problem whether our additive hardness of approximation result could be strengthened to a multiplicative bound if the computational resources are decreased from polynomial space to the more common setting of polynomial time.
|
|
| 10. |
- de Rezende, Susanna F., et al.
(författare)
-
The power of negative reasoning
- 2021
-
Ingår i: 36th Computational Complexity Conference, CCC 2021. - 1868-8969. - 9783959771931 ; 200
-
Konferensbidrag (refereegranskat)abstract
- Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.
|
|
