1. 
 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.


2. 
 Vinyals, Marc, et al.
(författare)

In between resolution and cutting planes : A study of proof systems for pseudoboolean 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. 292310

Konferensbidrag (refereegranskat)abstract
 We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflictdriven pseudoBoolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that socalled 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 treelike 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 pseudoBoolean solvers.


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


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. 866877

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 kclique. 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 stateoftheart algorithms for finding maximum cliques in graphs.


5. 
 Berkholz, C., et al.
(författare)

Supercritical spacewidth tradeoffs for resolution
 2016

Ingår i: Leibniz International Proceedings in Informatics, LIPIcs.  : Schloss Dagstuhl LeibnizZentrum 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 smallwidth resolution proof must have space exceeding by far the linear worstcase upper bound. This significantly strengthens the spacewidth tradeoffs in [Ben Sasson 2009], and provides one more example of tradeoffs 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 [BenSasson and Nordström 2008].


6. 
 Berkholz, Christoph, et al.
(författare)

Supercritical spacewidth tradeoffs for resolution
 2020

Ingår i: SIAM journal on computing (Print).  : Society for Industrial & Applied Mathematics (SIAM).  00975397 . 10957111. ; 49:1, s. 98118

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 smallwidth proof must have space exceeding by far the linear worstcase upper bound. This significantly strengthens the spacewidth tradeoffs in [E. BenSasson, SIAM J. Comput., 38 (2009), pp. 25112525], and provides one more example of tradeoffs 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. BenSasson 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. 709718].


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


8. 
 de Rezende, Susanna F.
(författare)

Lower Bounds and Tradeoffs 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 tradeoffs between different resources, such as length and space.A classical NPhard 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 kclique. In particular, this implies an unconditional lower bound on the running time of stateoftheartalgorithms for finding a maximum clique.In terms of trading resources, we prove a lengthspace tradeoff for the cutting planes proof system by first establishing a communicationround tradeoff for real communication via a roundaware simulation theorem. The technical contribution of this result allows us to obtain a separation between monotoneAC^(i1) and monotoneNC^i.We also obtain a tradeoff 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 sizedegree tradeoff 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 timespace tradeoffs 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 SizeDegree Tradeoffs from Reversible Pebbling
 2019

Ingår i: Proceedings of the 34th Annual Computational Complexity Conference (CCC ’19).  : Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing.  9783959771160 ; , s. 18:118: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 sizedegree tradeoffs 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 pseudoboolean solving
 2020

Ingår i: AAAI 2020  34th AAAI Conference on Artificial Intelligence.  : AAAI press. ; , s. 14951503

Konferensbidrag (refereegranskat)abstract
 PseudoBoolean solvers hold out the theoretical potential of exponential improvements over conflictdriven 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 nonnegligible but manageable overhead when detection is not successful, and yields significant gains for some SAT competition and crafted benchmarks for which pseudoBoolean reasoning is stronger than CDCL. It also boosts performance for some native pseudoBoolean formulas where this approach helps to improve learned constraints. Copyright

