Expansion-based QBF Solving on Tree Decompositions

• Autorzy: Charwat Günther , Woltran Stefan

Identyfikatory

DOI

10.3233/FI-2019-1810

• Języki publikacji: EN

Abstrakty

EN

In recent years various approaches for quantified Boolean formula (QBF) solving have been developed, including methods based on expansion, skolemization and search. Here, we present a novel expansion-based solving technique that is motivated by concepts from the area of parameterized complexity. Our approach relies on dynamic programming over the tree decomposition of QBFs in prenex conjunctive normal form (PCNF). Hereby, binary decision diagrams (BDDs) are used for compactly storing partial solutions. Towards efficiency in practice, we integrate dependency schemes and develop dedicated heuristic strategies. Our experimental evaluation reveals that our implementation is competitive to state-of-the-art solvers on instances with one quantifier alternation. Furthermore, it performs particularly well on instances up to a treewidth of approximately 80, even for more quantifier alternations. Results indicate that our approach is orthogonal to existing techniques, with a large number of uniquely solved instances.

Słowa kluczowe

EN

dynamic programming; expansion; QBF; quantified Boolean formula; QSAT; treewidth

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 167, nr 1-2
• Strony: 59--92
• Opis fizyczny: Bibliogr. 51 poz., rys., tab., wykr.

Twórcy

autor

Charwat Günther

• Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Vienna, Austria

autor

Woltran Stefan

• Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Vienna, Austria

Bibliografia

• [1] Stockmeyer LJ, Meyer AR. Word problems requiring exponential time (preliminary report). In: Proc. TOC. ACM, 1973 pp. 1-9.
• [2] Downey RG, Fellows MR. Parameterized Complexity. Monographs in Computer Science. Springer, 1999.
• [3] Chen H. Quantified constraint satisfaction and bounded treewidth. In: Proc. ECAI. IOS Press, 2004 pp.161-165. URL http://dblp.uni-trier.de/rec/bib/conf/ecai/Chen04.
• [4] Atserias A, Oliva S. Bounded-width QBF is PSPACE-complete. J. Comput. Syst. Sci., 2014. 80(7):1415-1429. URL http://dblp.uni-trier.de/rec/bib/journals/jcss/AtseriasO14.
• [5] Bryant RE. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986. 100(8):677-691.
• [6] Slivovsky F, Szeider S. Computing resolution-path dependencies in linear time. In: Proc. SAT, volume 7317 of LNCS. Springer, 2012 pp. 58-71. doi:10.1007/978-3-642-31612-8_6.
• [7] Pulina L. The ninth QBF solvers evaluation - preliminary report. In: Proc. QBF, volume 1719 of CEUR Workshop Proceedings. CEUR-WS.org, 2016 pp. 1-13. URL http://dblp.uni-trier.de/rec/bib/conf/sat/Pulina16.
• [8] Charwat G, Woltran S. Expansion-based QBF solving on tree decompositions. In: Proc. RCRA, volume 2011 of CEUR Workshop Proceedings. CEUR-WS.org, 2017 pp. 16-26.
• [9] Marin P, Narizzano M, Pulina L, Tacchella A, Giunchiglia E. An empirical perspective on ten years of QBF solving. In: Proc. RCRA, volume 1451 of CEUR Workshop Proceedings. CEUR-WS.org, 2015 pp.62-75. URL http://dblp.uni-trier.de/rec/bib/conf/aiia/MarinNPTG15.
• [10] Ayari A, Basin DA. QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Proc. FMCAD, volume 2517 of LNCS. Springer, 2002 pp. 187-201. doi:10.1007/3-540-36126-X_12.
• [11] Biere A. Resolve and expand. In: Proc. SAT, volume 3542 of LNCS. Springer, 2004 pp. 59-70. URL http://dblp.uni-trier.de/rec/bib/conf/sat/Biere04.
• [12] Janota M, Marques-Silva J. Abstraction-based algorithm for 2QBF. In: Proc. SAT, volume 6695 of LNCS. Springer, 2011 pp. 230-244. URL http://dblp.uni-trier.de/rec/bib/conf/sat/JanotaS11.
• [13] Janota M, Klieber W, Marques-Silva J, Clarke EM. Solving QBF with counterexample guided refinement. In: Proc. SAT, volume 7317 of LNCS. Springer, 2012 pp. 114-128. doi:10.1007/978-3-642-31612-8_10.
• [14] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 2003. 50(5):752-794. doi:10.1145/876638.876643.
• [15] Cadoli M, Giovanardi A, Schaerf M. An algorithm to evaluate quantified Boolean formulae. In: Proc. IAAI. AAAI Press / The MIT Press, 1998 pp. 262-267. URL http://dblp.uni-trier.de/rec/bib/conf/aaai/CadoliGS98.
• [16] Zhang L, Malik S. Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: Proc. CP, volume 2470 of LNCS. Springer, 2002 pp. 200-215. URL http://dblp.uni-trier.de/rec/bib/conf/cp/ZhangM02.
• [17] Giunchiglia E, Narizzano M, Tacchella A. Clause/term resolution and learning in the evaluation of quantified Boolean formulas. J. Artif. Intell. Res., 2006. 26:371-416. doi:10.1613/jair.1959.
• [18] Lonsing F, Biere A. DepQBF: A dependency-aware QBF solver. J. SAT, 2010. 7(2-3):71-76. URL http://dblp.uni-trier.de/rec/bib/journals/jsat/LonsingB10.
• [19] Lonsing F, Bacchus F, Biere A, Egly U, Seidl M. Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Proc. LPAR, volume 9450 of LNCS. Springer, 2015 pp. 418-433. doi:10.1007/978-3-662-48899-7_29.
• [20] Klieber W, Sapra S, Gao S, Clarke EM. A Non-prenex, non-clausal QBF solver with game-state learning. In: Proc. SAT, volume 6175 of LNCS. Springer, 2010 pp. 128-142. doi:10.1007/978-3-642-14186-7_12.
• [21] Bjørner N, Janota M, Klieber W. On conflicts and strategies in QBF. In: Proc. LPAR. Easy Chair, 2015 pp. 28-41. URL http://dblp.uni-trier.de/rec/bib/conf/lpar/BjornerJK15.
• [22] Pan G, Vardi MY. Symbolic decision procedures for QBF. In: Proc. CP, volume 3258 of LNCS. Springer, 2004 pp. 453-467. doi:10.1007/978-3-540-30201-8_34.
• [23] Jussila T, Sinz C, Biere A. Extended resolution proofs for symbolic SAT solving with quantification. In: Proc. SAT, volume 4121 of LNCS. Springer, 2006 pp. 54-60. doi:10.1007/11814948_8.
• [24] Pulina L, Tacchella A. Hard QBF encodings made easy: Dream or reality? In: Proc. AI*IA, volume 5883 of LNCS. Springer, 2009 pp. 31-41. doi:10.1007/978-3-642-10291-2_4.
• [25] Chen H, Dalmau V. From pebble games to tractability: An ambidextrous consistency algorithm for quantified constraint satisfaction. In: Proc. CSL, volume 3634 of LNCS. Springer, 2005 pp. 232-247. doi:10.1007/11538363_17.
• [26] Pulina L, Tacchella A. An empirical study of QBF encodings: From treewidth estimation to useful preprocessing. Fundam. Inform., 2010. 102(3-4):391-427. doi:10.3233/FI-2010-312.
• [27] Pulina L, Tacchella A. QuBIS: An (in)complete solver for quantified Boolean formulas. In: Proc. MICAI, volume 5317 of LNCS. Springer, 2008 pp. 34-43. doi:10.1007/978-3-540-88636-5_3.
• [28] Pulina L, Tacchella A. A structural approach to reasoning with quantified Boolean formulas. In: Proc. IJCAI. AAAI Press, 2009 pp. 596-602. URL http://dblp.uni-trier.de/rec/bib/conf/ijcai/PulinaT09.
• [29] Robertson N, Seymour PD. Graph minors. III. Planar tree-width. J. Comb. Theory, Ser. B, 1984. 36(1):49-64. doi:10.1016/0095-8956(84)90013-3.
• [30] Arnborg S, Corneil DG, Proskurowski A. Complexity of finding embeddings in a k-tree. SIAM J. Algebra. Discr. Meth., 1987. 8:277-284. doi:10.1137/0608024.
• [31] Bodlaender HL. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput., 1996. 25(6):1305-1317. doi:10.1137/S0097539793251219.
• [32] Bodlaender HL, Koster AMCA. Treewidth computations I. Upper bounds. Inf. Comput., 2010. 208(3):259-275. doi:10.1016/j.ic.2009.03.008.
• [33] Dechter R. Constraint Processing. Morgan Kaufmann, 2003.
• [34] Benedetti M. Quantifier trees for QBFs. In: Proc. SAT, volume 3569 of LNCS. Springer, 2005 pp. 378-385. doi:10.1007/11499107_28.
• [35] Ferrara A, Pan G, Vardi MY. Treewidth in verification: Local vs. global. In: Proc. LPAR, volume 3835 of LNCS. Springer, 2005 pp. 489-503. doi:10.1007/11591191_34.
• [36] Samer M, Szeider S. Backdoor sets of quantified Boolean formulas. J. Autom. Reasoning, 2009. 42(1):77-97. doi:10.1007/s10817-008-9114-5.
• [37] Lonsing F, Biere A. A compact representation for syntactic dependencies in QBFs. In: Proc. SAT, volume 5584 of LNCS. Springer, 2009 pp. 398-411.
• [38] Abseher M, Musliu N, Woltran S. Improving the efficiency of dynamic programming on tree decompositions via machine learning. J. Artif. Intell. Res., 2017. 58:829-858. doi:10.1007/978-3-642-02777-2_37.
• [39] Friedman SJ, Supowit KJ. Finding the optimal variable ordering for binary decision diagrams. In: Proc. DAC. ACM, 1987 pp. 348-356.
• [40] Somenzi F. CU Decision Diagram package release 3.0.0. Department of Electrical and Computer Engineering, University of Colorado at Boulder, 2015. URL http://vlsi.colorado.edu/~fabio/CUDD.
• [41] Abseher M, Musliu N, Woltran S. htd - A free, open-source framework for tree decompositions and beyond. Technical Report DBAI-TR-2016-96, TU Wien, 2016.
• [42] Biere A, Lonsing F, Seidl M. Blocked clause elimination for QBF. In: Proc. CADE, volume 6803 of LNCS. Springer, 2011 pp. 101-115. doi:10.1007/978-3-642-22438-6_10.
• [43] Rabe MN, Tentrup L. CAQE: A certifying QBF solver. In: Proc. FMCAD. IEEE, 2015 pp. 136-143. URL http://dblp.uni-trier.de/rec/bib/conf/fmcad/RabeT15.
• [44] Janota M, Marques-Silva J. Solving QBF by clause selection. In: Proc. IJCAI. AAAI Press, 2015 pp.325-331. URL http://dblp.uni-trier.de/rec/bib/conf/ijcai/JanotaM15.
• [45] Bogaerts B, Janhunen T, Tasharrofi S. Solving QBF instances with nested SAT solvers. In: Proc. Beyond NP, volume WS-16-05 of AAAI Workshops. AAAI Press, 2016. URL http://dblp.uni-trier.de/rec/bib/conf/aaai/0001JT16.
• [46] Scholl C, Pigorsch F. The QBF solver AIGSolve. In: Proc. QBF, volume 1719 of CEUR Workshop Proceedings. CEUR-WS.org, 2016 pp. 55-62. URL http://dblp.uni-trier.de/rec/bib/conf/sat/SchollP16.
• [47] Tu K, Hsu T, Jiang JR. QELL: QBF reasoning with extended clause learning and levelized SAT solving. In: Proc. SAT, volume 9340 of LNCS. Springer, 2015 pp. 343-359. doi:10.1007/978-3-319-24318-4_25.
• [48] Peitl T, Slivovsky F, Szeider S. Dependency learning for QBF. In: Proc. SAT, volume 10491 of LNCS. Springer, 2017 pp. 298-313. doi:10.1007/978-3-319-66263-3_19.
• [49] Goultiaeva A, Bacchus F. Recovering and utilizing partial duality in QBF. In: Proc. SAT, volume 7962 of LNCS. Springer, 2013 pp. 83-99. doi:10.1007/978-3-642-39071-5_8.
• [50] Wimmer R, Reimer S, Marin P, Becker B. HQSpre - An effective preprocessor for QBF and DQBF. In: Proc. TACAS, volume 10205 of LNCS. 2017 pp. 373-390. doi:10.1007/978-3-662-54577-5_21.
• [51] Lonsing F, Egly U. Evaluating QBF Solvers: Quantifier Alternations Matter. In: Proc. CP, volume 11008 of LNCS. Springer, 2018 pp. 276-294. doi:10.1007/978-3-319-98334-9_19.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).