| 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. |
- 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.
|
|
| 7. |
- 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.
|
|
| 8. |
- Elffers, Jan, et al.
(författare)
-
Divide and conquer : Towards faster pseudo-boolean solving
- 2018
-
Ingår i: IJCAI'18. - California : International Joint Conferences on Artificial Intelligence. ; , s. 1291-1299
-
Konferensbidrag (refereegranskat)abstract
- The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability-so-called SAT solvers-and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize-the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior. We propose a modified approach to pseudo-Boolean solving based on division instead of the saturation rule used in [Chai and Kuehlmann'05] and other PB solvers. In addition to resulting in a stronger conflict analysis, this also improves performance by keeping integer coefficient sizes down, and yields a very competitive solver as shown by the results in the Pseudo-Boolean Competitions 2015 and 2016.
|
|
| 9. |
- Gocht, Stephan, et al.
(författare)
-
On division versus saturation in pseudo-boolean solving
- 2019
-
Ingår i: IJCAI International Joint Conference on Artificial Intelligence. - California : International Joint Conferences on Artificial Intelligence Organization. ; , s. 1711-1718
-
Konferensbidrag (refereegranskat)abstract
- The conflict-driven clause learning (CDCL) paradigm has revolutionized SAT solving over the last two decades. Extending this approach to pseudo-Boolean (PB) solvers doing 0-1 linear programming holds the promise of further exponential improvements in theory, but intriguingly such gains have not materialized in practice. Also intriguingly, most PB extensions of CDCL use not the division rule in cutting planes as defined in [Cook et al.,'87] but instead the so-called saturation rule. To the best of our knowledge, there has been no study comparing the strengths of division and saturation in the context of conflict-driven PB learning, when all linear combinations of inequalities are required to cancel variables. We show that PB solvers with division instead of saturation can be exponentially stronger. In the other direction, we prove that simulating a single saturation step can require an exponential number of divisions. We also perform some experiments to see whether these phenomena can be observed in actual solvers. Our conclusion is that a careful combination of division and saturation seems to be crucial to harness more of the power of cutting planes
|
|
| 10. |
- Lauria, Massimo, et al.
(författare)
-
Tight Size-Degree Bounds for Sums-of-Squares Proofs
- 2017
-
Ingår i: Computational Complexity. - : SPRINGER BASEL AG. - 1016-3328 .- 1420-8954. ; 26:4, s. 911-948
-
Tidskriftsartikel (refereegranskat)abstract
- We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size for values of d = d(n) from constant all the way up to for some universal constant . This shows that the running time obtained by using the Lasserre semidefinite programming relaxations to find degree-d SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NP-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in Krajiek (Arch Math Log 43(4):427-441, 2004) and Dantchev & Riis (Proceedings of the 17th international workshop on computer science logic (CSL '03), 2003) and then applying a restriction argument as in Atserias et al. (J Symb Log 80(2):450-476, 2015; ACM Trans Comput Log 17:19:1-19:30, 2016). This yields a generic method of amplifying SOS degree lower bounds to size lower bounds and also generalizes the approach used in Atserias et al. (2016) to obtain size lower bounds for the proof systems resolution, polynomial calculus, and Sherali-Adams from lower bounds on width, degree, and rank, respectively.
|
|
