| 1. |
- 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].
|
|
| 2. |
- 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
|
|
| 3. |
- Elffers, Jan, et al.
(författare)
-
Justifying All Differences Using Pseudo-Boolean Reasoning
- 2020
-
Ingår i: Thirty-Fourth Aaai Conference On Artificial Intelligence, The Thirty-Second Innovative Applications Of Artificial Intelligence Conference And The Tenth Aaai Symposium On Educational Advances In Artificial Intelligence. - : ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE. ; , s. 1486-1494
-
Konferensbidrag (refereegranskat)abstract
- Constraint programming solvers support rich global constraints and propagators, which make them both powerful and hard to debug. In the Boolean satisfiability community, proof-logging is the standard solution for generating trustworthy outputs, and this has become key to the social acceptability of computer-generated proofs. However, reusing this technology for constraint programming requires either much weaker propagation, or an impractical blowup in proof length. This paper demonstrates that simple, clean, and efficient proof logging is still possible for the all-different constraint, through pseudo-Boolean reasoning. We explain how such proofs can be expressed and verified mechanistically, describe an implementation, and discuss the broader implications for proof logging in constraint programming.
|
|
| 4. |
- Lagarde, G., et al.
(författare)
-
Trade-offs between size and degree in polynomial calculus
- 2020
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. ; 151
-
Konferensbidrag (refereegranskat)abstract
- Building on [Clegg et al.’96], [Impagliazzo et al.’99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(n log S). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen’16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.
|
|
| 5. |
- Risse, Kilian, 1991-
(författare)
-
On Long Proofs of Simple Truths
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Propositional proof complexity is the study of certificates of infeasibility. In this thesis we consider several proof systems with limited deductive ability and unconditionally show that they require long refutations of the feasibility of certain Boolean formulas. We show that the depth $d$ Frege proof system, restricted to linesize $M$, requires proofs of length at least $\exp\bigl(n/(\log M)^{O(d)}\bigr)$ to refute the Tseitin contradiction defined over the $n \times n$ grid graph, improving upon the recent result of Pitassi et al. [PRT21]. Along the way we also sharpen the lower bound of Håstad [Hås20] on the depth $d$ Frege refutation size for the same formula from exponential in $\tilde{\Omega}(n^{1/59d})$ to exponential in$\tilde{\Omega}(n^{1/(2d-1)})$. We also consider the perfect matching formula defined over a sparse random graph on an odd number of vertices $n$. We show that polynomial calculus over fields of characteristic $\neq 2$ and sum of squares require size exponential in $\Omega(n/\log^2 n)$ to refute said formula. For depth $d$ Frege we show that there is a constant $\delta > 0$ such that refutations of these formulas require size $\exp\bigl(\Omega(n^{\delta/d})\bigl)$. The perfect matching formula has a close sibling over bipartite graphs: the graph pigeonhole principle. There are two methods to prove resolution refutation size lower bounds for the pigeonhole principle. On the one hand there is the general width-size tradeoff by Ben-Sasson and Wigderson [BW01] which can be used to show resolution refutation size lower bounds in the setting where we have a sparse bipartite graph with $n$ holes and $m \ll n^2$pigeons. On the other hand there is the pseudo-width technique developed by Razborov [Raz04] that applies for any number of pigeons, but requires the graph to be somewhat dense. We extend the latter technique to also cover the previous setting and more: for example, it has been open whether the functional pigeonhole principle defined over a random bipartite graph of bounded degree and $\poly(n) \ge n^2$ pigeons requires super-polynomial size resolution refutations. We answer this and related questions. Finally we also study the circuit tautology which claims that a Boolean function has a circuit of size $s$ computing it. For $s = \poly(n)$ we prove an essentially optimal Sum of Squares degree lower bound of $\Omega(s^{1-\eps})$ to refute this claim for any Boolean function. Further, we show that for any $0 < \alpha < 1$ there are Boolean functions on $n$ bits with circuit complexity larger than$2^{n^\alpha}$ but the Sum of Squares proof system requires size $2^{\bigl(2^{\Omega(n^\alpha)}\bigr)}$ to prove this. Lastly we show that these lower bounds can also be extended to the monotone setting.
|
|
