Dependency Schemes in QBF Calculi: Semantics and Soundness?

Abstract

We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use it to express a property of dependency schemes called full exhibition that is known to be su cient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhibition remains su cient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the re exive resolution path dependency scheme is fully exhibited.

Introduction

The excellent success of SAT solvers in the realm of propositional Boolean formulae has motivated much interest in the corresponding search problem for quantied Boolean formulae (QBF). The greater expressiveness of QBF, a orded by its PSPACE-completeness [ 23 ], presents novel challenges in solving, and the array of emerging techniques is motivating a wealth of research in the closely-related eld of proof complexity [3, 5{9, 11{14].

There is a natural correspondence between QBF practice and proof theory; when a solver concludes the falsity of an instance, the trace can be interpreted as a formal refutation. Understanding the refutational proof system that underpins a particular solving method, and thereby accounts for its correctness, motivates the proof-theoretic study of speci c calculi. Recent work has led to a complete understanding of the relative strength of resolution-based QBF systems [ 3, 7 ], including Q-resolution (Q-Res) [ 15 ], universal Q-resolution (QU-Res) [ 13 ], and long-distance Q-resolution (LD-Q-Res) [ 1 ].

Implemented in the state-of-the-art solver DepQBF [ 16,17 ], one of the recent and exciting developments in QBF solving has seen the introduction of dependency schemes : algorithms that gather information on variable independence by prior appeal to the syntactic form of an instance. The quanti er pre x of a QBF (in prenex normal form) imposes a total order on the variables; due to the ? This is an extended abstract of the paper published in the proceedings of CP 2016 [ 4 ] nesting of quanti er scopes, the value of a Boolean variable z can be dependent upon the variables to its left in the pre x. Naturally, this entails some restrictions on solving methods, and on the rules of the related formal systems. In general, however, z does not necessarily depend on all of the variables to its left. A dependency scheme attempts to replace the linear order of the pre x with a partial order that more accurately re ects the dependency structure of the formula, by identi ying variable independence. This approach allows some sets of instances to be solved more e eciently, despite the compuational overhead of computing the dependency scheme [ 16 ].

Independence itself is presented as a semantic concept [ 16, 18 ]. The truth of a QBF is witnessed by a Skolem-function model, a set of Boolean functions ffxg that produce a propositional tautology when substituted for the existential variables. The arguments to fx are the universal variables Ux left of x in the quanti er pre x, but it may occur that some circuit computes fx without using u 2 Ux as an input. In this case we say that x is independent of u { and a dual notion for false QBFs provides for independence of universals on existentials { even though the Skolem-function model is in general not unique.

This lack of uniqueness has consequences for soundness in QBF calculi. The impact of a dependency scheme in the proof system is to allow some logical steps which previously were prohibited; speci cally, the 8-reduction rule of Q-Res receives greater reign. This motivated the proposal of Q(D)-Res by Slivovsky and Szeider [ 22 ], a parametrization of the classical calculus by dependency schemes. Some schemes which were previously put forward in the literature, such as the triangle [ 19 ] and resolution path [ 24 ] dependency schemes, have proved too aggressive for soundness in Q(D)-Res, admitting refutations of true QBFs. The reexive resolution path dependency scheme [ 22 ] is currently the strongest known scheme for which Q(D)-Res is sound, a result which was proved by means of a di cult transformation of a Q(D)-Res refutation into a Q-Res refutation [ 22 ].

What is currently absent in the literature is a deeper understanding of soundness based on classi cation of dependency schemes; moreover, the lack of general methods may frustrate future developments. It is natural to propose the parametrization by dependency schemes of stronger QBF calculi, of the other CDCL-based QBF resolution systems and QBF Frege [ 5 ], whereupon methods for proving soundness based on properties of dependency schemes will carry over. In this paper we demonstrate that semantic notions of independence are indeed equipped for this; our contributions are summarized below. 1. New QBF calculi parametrized by dependency schemes. We extend the parametrisation by dependency schemes to all the CDCL-based resolution calculi for QBF: with the new long-distance calculus LD-Q(D)-Res, with universal resolution QU(D)-Res, and with their combination LQU(D)-Res. Our new long-distance calculus presents the greatest challenge. Of the two inference rules employed classically, parametrization of 8-reduction can be lifted straight from Q(D)-Res; here we investigate the additional e ects of parametrizing the longdistance resolution rule as well, by relaxing the conditions under which so-called `merged literals' can be introduced. Progressing from Q-resolution, we demonstrate that variable independence and merging have a more subtle interaction; in LD-Q(D)-Res, we must supplant merged literals with annotated literals, which record existential pivots to prevent unsound 8-reduction steps. 2. A semantic framework for independence and soundness. We unify some existing approaches in the literature towards a more fruitful understanding of the interplay between Q-resolution and dependency schemes. Building on the work of Samer [ 18 ] and Lonsing [ 16 ] we propose a semantic framework for variable independence. Central to the framework is a property of dependency schemes called full exhibition, which was shown to be su cient for soundness in Q(D)-Res by Slivovsky [ 21 ]. We further the potential of this approach to show that full exhibition is su cient for soundness in all the dependency calculi we introduce. To that end, we handle the semantic obstacles of long-distance resolution by incorporating techniques from strategy extraction due to Balabanov et al. [ 2 ]. 3. Demonstrating full exhibition. We conclude by proving Slivovsky's conjecture [21, p. 37] that the re exive resolution path dependency scheme Drrs is fully exhibited. Currently, Drrs is arguably the most important dependency scheme, capable of revealing more cases of independence than any other tractable scheme known to be sound for Q(D)-Res. As such, we show that everything currently known about soundness in this setting can be explained by full exhibition. On the technical level, the result is obtained by an algorithmic transformation of an arbitrary model for a true QBF into a model that exhibits all the required independencies. We therefore reveal the possibility for QBF solving to implement long-distance techniques fully parametrized by Drrs, or any other fully exhibited scheme. 2

Preliminaries

Quanti ed Boolean Formulas. A Quanti ed Boolean Formula (QBF) over a set V = fz1; : : : ; zng of n variables is a formula in quanti ed Boolean logic with variables ranging over f0; 1g. We consider only formulas in prenex conjunctive normal form (PCNF), denoted = Q . , in which all variables are quanti ed either existentially or universally in the quanti er pre x Q = Q1z1 Qnzn, Qi 2 f9; 8g for i 2 [n], and is a propositional conjunctive normal form (CNF) formula called the matrix. A CNF matrix is a conjunction of clauses, each clause is a disjunction of literals, and a literal is a variable or its negation. Whenever convenient, we refer to a clause as a set of literals and to a matrix as a set of clauses. We typically write x for existential variables, u and v for universals, and z for either. We denote the sets of existentially and universally quanti ed variables of by V9 = fzi 2 V j Qi = 9g and V8 = fzi 2 V j Qi = 8g respectively. The pre x Q imposes a linear ordering < on the variables of , such that zi < zj holds whenever i < j, in which case we say that zj is right of zi, or that zi is left of zj . The sets of variables right and left of z are denoted R (z) = fz0 2 V j z < z0g and L (z) = fz0 2 V j z0 < zg.

Assignment Trees and Models. Assignment trees for PCNF were rst introduced in [ 20 ]. We represent an assignment tree formally as a set of paths. Let be a PCNF over variables V = fz1; : : : ; zng and let V8 = fu1; : : : ; ukg. A path is a set of literals P = fl1; : : : ; lng with var(li) = zi for all i 2 [n], and we write P [zi] = li. A set of paths T is well-formed for i (1) for all u 2 V8 and for all P; Q 2 T , if P [v] = Q[v] for all v 2 L (u) \ V8, then P [x] = Q[x] for each x 2 L (u) \ V9, and (2) there is a unique path P 2 T with U P for each set of literals U = fl1; : : : ; lkg such that var(li) = ui for i 2 [k]. A set of paths that is well-formed for is an assignment tree for . We also use P to denote the total assignment P : V ! f>; ?g given by P (zi) = ? if li = :zi and P (zi) = > if li = zi, and extend this notation to literals with P (:zi) = :P (zi), where > = :? and vice versa. An assignment tree for is a model for , typically denoted M , i P (C) = > for all paths P 2 T and all clauses C 2 , where P (C) = > i P (l) = > for some l 2 C. A PCNF which has a model is true, otherwise it is false. An assignment tree is depicted as a tree with root r. Dependency Schemes. The trivial dependency scheme Dtrv is a mapping which associates each PCNF = Q1z1 Qnzn . over variables V to the trivial dependency relation Dtrv = f(zi; zj ) j i < j and Qi 6= Qj g. A proto-dependency scheme1 D is a function that maps each PCNF to a binary relation D Dtrv called the dependency relation. If (zi; zj ) 2 D , then (zi; zj ) is a D-dependency and zj is a D-dependent of zi, otherwise zj is D-independent of zi. A protodependency scheme D0 is said to be at least as general as another D if D0 D for all PCNFs , and is strictly more general if the inclusion is strict for some formula. For a PCNF over variables V and u 2 V8, we write D (u) = f(u; x) j x 2 V9 and (u; x) 2= D g.

QBF Resolution Calculi. We give a brief overview of four resolution-based CDCL QBF calculi { see [ 7 ] for a more detailed survey. A refutational QBF calculus is sound i the empty clause cannot be derived from any true formula.

Q-resolution (Q-Res) introduced in [ 15 ] is the standard refutational calculus for PCNF. In addition to resolution over existential pivots with non-tautologous resolvents, the calculus has a universal reduction rule which allows a clause C to be derived from C [ fug, where u is a universal literal and all existential literals in C are left of u. QU-resolution (QU-Res) [ 13 ] is a natural extension of Q-Res that allows universal resolution pivots.

Long-distance resolution, which was introduced in [ 25 ] and formalised as the calculus LD-Q-Res [ 1 ], allows tautologous resolvents under certain conditions, 1 The term `dependency scheme' was rst introduced to denote a subset of protodependency schemes with a more technical de nition [ 19 ]; for consistency with the literature we will use `proto-dependency scheme' in technical portions of this paper. using the special merged literal u to represent the tautology fu; :ug. The resulting system is exponentially stronger than Q-Res [ 12 ]. Finally, the calculus LQU-Res [ 3 ] combines naturally the features of QU-Res and LD-Q-Res, allowing merged literals and resolution over universal pivots. 3

Our Contributions

In this section, we give a brief survey of the contributions contained in the fulllength version of the paper [ 4 ], to which we refer the reader for proofs and further detailed commentry. 3.1

A Semantic Framework and New QBF Calculi We reformulate the de nition of independence in terms of assignment trees from [ 16, 18 ]; we feel our notation is better suited to the aims of the current work. We introduce the new idea of complementary paths in an assignment tree, and de ne a property of dependency schemes called full exhibition.

De nition 1 (Complementary path). Let be a QBF over variables V , let U be a non-tautologous set of literals such that var(U ) = V8, let T be an assignment tree for and let P 2 T be the unique path such that U P . Then, for any u 2 V8, Pu 2 T is the unique path such that U 0 Pu, where U 0 = (U n flg) [ f:lg, l 2 U and var(l) = u.

De nition 2 (Independence of existentials from universals [ 16,18 ]). Let be a true QBF over variables V and let u 2 V8, x 2 V9. We say that x is independent of u in if there exists a model M for in which P (x) = Pu(x) for all paths P 2 M . For such a model M we write M (u; x), and we say that M exhibits the independence of x from u in .

De nition 3 (Fully exhibited dependency scheme). Let D be a protodependency scheme. We say that D is fully exhibited i for each true PCNF there is a model M for such that M (u; x) for each pair (u; x) 2= D , with u 2 V8 and x 2 V9.

In [ 21 ], it was proved that Q(D)-Res is sound for fully exhibited2 D, and this was combined with the fact that the standard dependency scheme Dstd is fully exhibited (attributed to [ 10 ]). We show that this approach scales up to the dependency versions of stronger QBF calculi. To do this, we introduce the new long-distance calculi LD-Q(D)-Res and LQU(D)-Res (Fig. 1), the respective dependency versions of LD-Q-Res and LQU-Res. Parametrising long-distance resolution calls for the introduction of annotations that prevent unsound 8-reduction steps. 2 Full exhibition is treated equivalently, as a property of models.

(Axiom) D [ fuX g (8-Red)

D

C is a clause in the matrix of .

Variable u is universal. If l 2 D and var(l) = z, then (u; z) 2= D , and if l = zX0 then (u; x) 2= D for all x 2 X0. If X = ; then literal uX is either u or :u.

C1 [ U1 [ fxg C2 [ U2 [ f:xg (Res)

C1 [ C2 [ U If for l1 2 C1; l2 2 C2; var(l1) = var(l2), then l1 = l2 is not annotated. var(U1) = var(U2) V8, and (x; u) 2= D for each u 2 var(U1). If for u1 2 U1; u2 2 U2; var(u1) = var(u2) = u, then u1 = :u2; or at least one of u1; u2 is annotated. U is de ned as fuX j u 2 var(U1)g, where X is the union of fxg with any annotations on u in U1 [ U2. In LD-Q(D)-Res var(x) is existential. In LQU(D)-Res, var(x) is existential or universal. We rst prove that full exhibition is a su cient condition for soundness in the new long-distance QBF calculi.

Theorem 4. Let D be a fully exhibited proto-dependency scheme. Then LDQ(D)-Res is sound.

Since the (omitted) proof of Theorem 4 makes no use of the fact that the pivot is existential, it also shows the soundness of LQU(D)-Res, the `dependency version' of LQU-Res, for any fully exhibited D.

Theorem 5. Let D be a fully exhibited proto-dependency scheme. Then LQU(D)Res is sound.

Also, since LQU(D)-Res clearly simulates QU(D)-Res simply by disallowing longdistance resolution steps, we obtain the same result for QU(D)-Res. Theorem 6. Let D be a fully exhibited proto-dependency scheme. Then QU(D)Res is sound.

Theorems 4, 5 and 6 together constitute the generalisation to all the CDCL QBF calculi of Slivovsky's result [ 21 ] that Q(D)-Res is sound for fully exhibited D. Whereas full exhibition is a su cient condition for each calculus, it is not a necessary condition for any of them.

Proposition 7. There exists a proto-dependency scheme D that is not fullyexhibited for which LQU(D)-Res is sound.

For proof of concept, we demonstrate that the re exive resolution path dependency scheme Drrs [ 22 ] is fully exhibited, thereby proving the conjecture of Slivovsky [21, p.37]. This result provides a better understanding of soundness in Q-resolution with dependency schemes; since Drrs is the most general scheme known to be sound in Q(D)-Res, what is already known about soundness for that calculus can subsequently be explained entirely by full exhibition. Theorem 8. Drrs is fully exhibited.

Our concluding result now follows immediately from Theorems 4, 5 and 6. Corollary 9. QU(Drrs)-Res, LD-Q(Drrs)-Res and LQU(Drrs)-Res are sound proof systems. 4

Conclusions

As we have shown, the parametrization by dependency schemes can be extended to all four CDCL QBF calculi, and the property of full exhibition { which is possessed by the re exive resolution path dependency scheme { is su cient for soundness in each case. Showing by counterexample that full-exhibition is not a necessary condition, our work leads naturally to the open problem of nding a characterization for soundness in this setting.

Acknowledgments. This research was supported by grant no. 48138 from the John Templeton Foundation and EPSRC grant EP/L024233/1.

References

1. Balabanov , V. , Jiang , J.R. : Uni ed QBF certi cation and its applications . Formal Methods in System Design 41 ( 1 ), 45 { 65 ( 2012 )

2. Balabanov , V. , Jiang , J.R. , Janota , M. , Widl , M.: E cient extraction of QBF (counter)models from long-distance resolution proofs . In: Conference on Arti cial Intelligence (AAAI) . pp. 3694 { 3701 ( 2015 )

3. Balabanov , V. , Widl , M. , Jiang , J.R.: QBF resolution systems and their proof complexities . In: International Conference on Theory and Applications of Satis ability Testing (SAT) . pp. 154 { 169 ( 2014 )

4. Beyersdor , O. , Blinkhorn , J.: Dependency schemes in QBF calculi: Semantics and soundness . In: Principles and Practice of Constraint Programming (CP) . pp. 96 { 112 ( 2016 )

5. Beyersdor , O. , Bonacina , I. , Chew , L. : Lower bounds: From circuits to QBF proof systems . In: ACM Conference on Innovations in Theoretical Computer Science (ITCS) . pp. 249 { 260 ( 2016 )

6. Beyersdor , O. , Chew , L. , Janota , M. : On uni cation of QBF resolution-based calculi . In: International Symposium on Mathematical Foundations of Computer Science (MFCS) . pp. 81 { 93 ( 2014 )

7. Beyersdor , O. , Chew , L. , Janota , M. : Proof complexity of resolution-based QBF calculi . In: International Symposium on Theoretical Aspects of Computer Science (STACS) . Leibniz International Proceedings in Informatics (LIPIcs) , vol. 30 , pp. 76 { 89 ( 2015 )

8. Beyersdor , O. , Chew , L. , Mahajan , M. , Shukla , A. : Feasible interpolation for QBF resolution calculi . In: International Colloquium on Automata, Languages, and Programming (ICALP) . pp. 180 { 192 ( 2015 )

9. Beyersdor , O. , Chew , L. , Mahajan , M. , Shukla , A. : Are short proofs narrow? QBF resolution is not simple . In: Symposium on Theoretical Aspects of Computer Science (STACS) . pp. 15 : 1 { 15 : 14 ( 2016 )

10. Bubeck , U. : Model-based transformations for quanti ed boolean formulas ( 2010 )

11. Egly , U. : On sequent systems and resolution for QBFs . In: International Conference on Theory and Applications of Satis ability Testing (SAT) . pp. 100 { 113 ( 2012 )

12. Egly , U. , Lonsing , F. , Widl , M. : Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving . In: International Conference on Logic for Programming , Arti cial Intelligence and Reasoning (LPAR) . pp. 291 { 308 ( 2013 )

13. Gelder , A.V. : Contributions to the theory of practical quanti ed boolean formula solving . In: International Conference on Principles and Practice of Constraint Programming (CP) . pp. 647 { 663 ( 2012 )

14. Janota , M. , Marques-Silva , J. : Expansion-based QBF solving versus Q-resolution . Theorical Compututer Science 577 , 25 { 42 ( 2015 )

15. Kleine Buning, H., Karpinski , M. , Flogel, A.: Resolution for quanti ed boolean formulas . Information and Computation 117 ( 1 ), 12 { 18 ( 1995 )

16. Lonsing , F. : Dependency Schemes and Search-Based QBF Solving: Theory and Practice . Ph.D. thesis , Johannes Kepler University ( 2012 )

17. Lonsing , F. , Egly , U. : Incrementally computing minimal unsatis able cores of QBFs via a clause group solver API . In: International Conference on Theory and Applications of Satis ability Testing (SAT) . pp. 191 { 198 ( 2015 )

18. Samer , M. : Variable dependencies of quanti ed csps . In: International Conference on Logic for Programming , Arti cial Intelligence and Reasoning (LPAR) . pp. 512 { 527 ( 2008 )

19. Samer , M. , Szeider , S. : Backdoor sets of quanti ed boolean formulas . Journal of Automated Reasoning 42 ( 1 ), 77 { 97 ( 2009 )

20. Samulowitz , H. , Bacchus , F. : Using SAT in QBF . In: International Conference on Principles and Practice of Constraint Programming (CP) . pp. 578 { 592 ( 2005 )

21. Slivovsky , F. : Structure in #SAT and QBF . Ph.D. thesis , Vienna University of Technology ( 2015 )

22. Slivovsky , F. , Szeider , S. : Soundness of Q-resolution with dependency schemes . TCS 612 , 83 { 101 ( 2016 )

23. Stockmeyer , L.J., Meyer, A.R. : Word problems requiring exponential time: Preliminary report . In: Annual Symposium on Theory of Computing . pp. 1 { 9 . ACM ( 1973 )

24. Van Gelder , A. : Variable independence and resolution paths for quanti ed boolean formulas . In: International Conference on Principles and Practice of Constraint Programming (CP) . pp. 789 { 803 . Springer ( 2011 )

25. Zhang , L. , Malik , S. : Con ict driven learning in a quanti ed boolean satis ability solver . In: International Conference on Computer-aided Design (ICCAD) . pp. 442 { 449 ( 2002 )