| 1. |
- Elffers, Jan, et al.
(författare)
-
Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean 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. 75-93
-
Konferensbidrag (refereegranskat)abstract
- We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like 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 real-valued 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 pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.
|
|
| 2. |
- Vinyals, Marc, et al.
(författare)
-
In between resolution and cutting planes : A study of proof systems for pseudo-boolean SAT solving
- 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. 292-310
-
Konferensbidrag (refereegranskat)abstract
- We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP—which would require major technical breakthroughs in proof complexity—these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers.
|
|
| 3. |
- 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.
|
|
| 4. |
- 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.
|
|
| 5. |
- Berkholz, C., et al.
(författare)
-
Supercritical space-width trade-offs for resolution
- 2016
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. - 9783959770132
-
Konferensbidrag (refereegranskat)abstract
- We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben- Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].
|
|
| 6. |
- Berkholz, Christoph, et al.
(författare)
-
Supercritical space-width trade-offs for resolution
- 2020
-
Ingår i: SIAM journal on computing (Print). - : Society for Industrial & Applied Mathematics (SIAM). - 0097-5397 .- 1095-7111. ; 49:1, s. 98-118
-
Tidskriftsartikel (refereegranskat)abstract
- We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [E. Ben-Sasson, SIAM J. Comput., 38 (2009), pp. 2511-2525], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [A.A. Razborov, J. ACM, 63 (2016), 16]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [E. Ben-Sasson and J. Nordström, Short proofs may be spacious: An optimal separation of space and length in resolution, in Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS '08), 2008, pp. 709-718].
|
|
| 7. |
- 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.
|
|
| 8. |
- de Rezende, Susanna F.
(författare)
-
Lower Bounds and Trade-offs in Proof Complexity
- 2019
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Propositional proof complexity is a field in theoretical computer science that analyses the resources needed to prove statements. In this thesis, we are concerned about the length of proofs and trade-offs between different resources, such as length and space.A classical NP-hard problem in computational complexity is that of determining whether a graph has a clique of size k. We show that for all k ≪ n^(1/4) regular resolution requires length n^Ω(k) to establish that an Erdős–Rényi graph with n vertices and appropriately chosen edge density does not contain a k-clique. In particular, this implies an unconditional lower bound on the running time of state-of-the-artalgorithms for finding a maximum clique.In terms of trading resources, we prove a length-space trade-off for the cutting planes proof system by first establishing a communication-round trade-off for real communication via a round-aware simulation theorem. The technical contri-bution of this result allows us to obtain a separation between monotone-AC^(i-1) and monotone-NC^i.We also obtain a trade-off separation between cutting planes (CP) with unbounded coefficients and cutting planes where coefficients are at most polynomial in thenumber of variables (CP*). We show that there are formulas that have CP proofs in constant space and quadratic length, but any CP* proof requires either polynomial space or exponential length. This is the first example in the literature showing any type of separation between CP and CP*.For the Nullstellensatz proof system, we prove a size-degree trade-off via a tight reduction of Nullstellensatz refutations of pebbling formulas to the reversible pebbling game. We show that for any directed acyclic graph G it holds that G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatzrefutation of the pebbling formula over G in size t + 1 and degree s.Finally, we introduce the study of cumulative space in proof complexity, a measure that captures the space used throughout the whole proof and not only the peak space usage. We prove cumulative space lower bounds for the resolution proof system, which can be viewed as time-space trade-offs where, when time is bounded, space must be large a significant fraction of the time.
|
|
| 9. |
- de Rezende, Susanna F., et al.
(författare)
-
Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling
- 2019
-
Ingår i: Proceedings of the 34th Annual Computational Complexity Conference (CCC ’19). - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. - 9783959771160 ; , s. 18:1-18:16
-
Konferensbidrag (refereegranskat)abstract
- We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if an only if there is a Nullstellensatz refutation of the pebbling formula over G in size t + 1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.
|
|
| 10. |
- Elffers, J., et al.
(författare)
-
A cardinal improvement to pseudo-boolean solving
- 2020
-
Ingår i: AAAI 2020 - 34th AAAI Conference on Artificial Intelligence. - : AAAI press. ; , s. 1495-1503
-
Konferensbidrag (refereegranskat)abstract
- Pseudo-Boolean solvers hold out the theoretical potential of exponential improvements over conflict-driven clause learning (CDCL) SAT solvers, but in practice perform very poorly if the input is given in the standard conjunctive normal form (CNF) format. We present a technique to remedy this problem by recovering cardinality constraints from CNF on the fly during search. This is done by collecting potential building blocks of cardinality constraints during propagation and combining these blocks during conflict analysis. Our implementation has a non-negligible but manageable overhead when detection is not successful, and yields significant gains for some SAT competition and crafted benchmarks for which pseudo-Boolean reasoning is stronger than CDCL. It also boosts performance for some native pseudo-Boolean formulas where this approach helps to improve learned constraints. Copyright
|
|
