1. 
 Alwen, Joël, et al.
(författare)

Cumulative Space in BlackWhite Pebbling and Resolution
 2017

Ingår i: Leibniz International Proceedings in Informatics, LIPIcs.  : Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing.  9783959770293

Konferensbidrag (refereegranskat)abstract
 We study space complexity and timespace tradeoffs 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 blackwhite pebble game and prove optimal cumulative space lower bounds and tradeoffs, 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 1015 years. Using and extending the connection between proof complexity and pebble games in [BenSasson 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. 
 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. 466485

Konferensbidrag (refereegranskat)abstract
 We consider the pebble game on DAGs with bounded fanin 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 PSPACEcomplete, 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 PSPACEhard 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 PSPACEhard 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.


3. 
 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. 295304

Konferensbidrag (refereegranskat)abstract
 We obtain the first true sizespace tradeoffs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constantsize 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 tradeoffs to hold uniformly for resolution, polynomial calculus and cutting planes, thus capturing the main methods of reasoning used in current stateoftheart SAT solvers. We prove our results by a reduction to communication lower bounds in a roundefficient 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 tradeoffs between cost and number of rounds in the game of [Dymond and Tompa '85] played on directed acyclic graphs. As a byproduct of the techniques developed to show these proof complexity tradeoff results, we also obtain an exponential separation between monotoneAC(i1) and monotoneAC(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(i1) n) require exponential size.


4. 
 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 greaterthan. 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 nonexplicit 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.


5. 
 De Rezende, Susanna, et al.
(författare)

Lifting with simple gadgets and applications to circuit and proof complexity
 2020

Ingår i: Proceedings  2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020.  02725428.  9781728196213  9781728196220 ; 2020November, s. 2430

Konferensbidrag (refereegranskat)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 greaterthan. We apply our generalized theorem to solve three 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 subpolynomial line 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 nonexplicit separation was known. •We give the strongest separation todate between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomialsize monotone Boolean circuits, requires monotone Boolean formulas of size 2{Omega(n text{polylog}(n))}. 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. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144.


6. 
 Elffers, Jan, et al.
(författare)

Tradeoffs between time and memory in a tighter model of CDCL SAT solvers
 2016

Ingår i: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016.  Cham : Springer.  9783319409696 ; , s. 160176

Konferensbidrag (refereegranskat)abstract
 A long line of research has studied the power of conflict driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot ten, and the polynomial blowup is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more finegrained model of CDCL that cap tures not only time but also memory usage and number of restarts. We show how previously established strong sizespace tradeoffs for resolution can be transformed into equally strong tradeoffs between time and memory usage for CDCL, where the upper bounds hold for CDCL with out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.


7. 
 Elffers, Jan, et al.
(författare)

Using combinatorial benchmarks to probe the reasoning power of pseudoboolean solvers
 2018

Ingår i: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018.  Cham : Springer.  9783319941431 ; , s. 7593

Konferensbidrag (refereegranskat)abstract
 We study cdclcuttingplanes, OpenWBO, and Sat4j, three successful solvers from the PseudoBoolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudoBoolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in stateoftheart PB solving techniques. Although our benchmarks have linearsize treelike CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also realvalued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudoBoolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current stateoftheart PB solving.


8. 
 Filmus, Y., et al.
(författare)

From small space to small width in resolution
 2014

Ingår i: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014).  : Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing.  9783939897651 ; , s. 300311

Konferensbidrag (refereegranskat)abstract
 In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a byproduct, we develop a "blackbox" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutationprevious techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.


9. 
 Filmus, Yuval, et al.
(författare)

Towards an understanding of polynomial calculus : New separations and lower bounds (extended abstract)
 2013

Ingår i: Automata, Languages, and Programming.  Berlin, Heidelberg : Springer.  9783642392054 ; , s. 437448

Konferensbidrag (refereegranskat)abstract
 During the last decade, an active line of research in proof complexity has been into the space complexity of proofs and how space is related to other measures. By now these aspects of resolution are fairly well understood, but many open problems remain for the related but stronger polynomial calculus (PC/PCR) proof system. For instance, the space complexity of many standard "benchmark formulas" is still open, as well as the relation of space to size and degree in PC/PCR. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PCR space, providing some circumstantial evidence that degree might be a lower bound for space. More importantly, this immediately yields formulas that are very hard for space but very easy for size, exhibiting a sizespace separation similar to what is known for resolution. Using related ideas, we show that if a graph has good expansion and in addition its edge set can be partitioned into short cycles, then the Tseitin formula over this graph requires large PCR space. In particular, Tseitin formulas over random 4regular graphs almost surely require space at least Ω(√n). Our proofs use techniques recently introduced in [BonacinaGalesi '13]. Our final contribution, however, is to show that these techniques provably cannot yield nonconstant space lower bounds for the functional pigeonhole principle, delineating the limitations of this framework and suggesting that we are still far from characterizing PC/PCR space.


10. 
 Lauria, M., et al.
(författare)

CNFgen : A generator of crafted benchmarks
 2017

Ingår i: 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017.  Cham : Springer.  9783319662626 ; , s. 464473

Konferensbidrag (refereegranskat)abstract
 We present CNFgen, a generator of combinatorial benchmarks in DIMACS and OPB format. The proof complexity literature is a rich source not only of hard instances but also of instances that are theoretically easy but “extremal” in different ways, and therefore of potential interest in the context of SAT solving. Since most of these formulas appear not to be very well known in the SAT community, however, we propose CNFgen as a resource to make them readily available for solver development and evaluation. Many formulas studied in proof complexity are based on graphs, and CNFgen is also able to generate, parse and do basic manipulation of such objects. Furthermore, it includes a library cnfformula giving access to the functionality of CNFgen to Python programs.

