Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. (English) Zbl 1522.68715
Summary: In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the \(\forall\)Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
References:
| [1] | Alur R, Bodík R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2015) Syntax-guided synthesis. In: Dependable Software Systems Engineering, volume 40 of NATO Science for Peace and Security Series, D: Information and Communication Security. IOS Press, pp 1-25 |
| [2] | Audemard G, Simon L (2009) Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, pp 399-404 |
| [3] | Ayari A, Basin DA (2002) QUBOS: deciding quantified Boolean logic using propositional satisfiability solvers. In: FMCAD, volume 2517 of LNCS. Springer, pp 187-201 · Zbl 1019.68597 |
| [4] | Balabanov V, Jiang J-HR, Scholl C, Mishchenko A, Brayton RK (2016) 2QBF: challenges and Solutions. In: SAT, volume 9710 of LNCS. Springer, pp 453-469 · Zbl 1475.68335 |
| [5] | Balyo, T.; Biere, A.; Iser, M.; Sinz, C., SAT Race 2015, Artif Intell, 241, 45-65 (2016) · Zbl 1392.68381 · doi:10.1016/j.artint.2016.08.007 |
| [6] | Beyersdorff O, Chew L, Janota M (2014) On unification of QBF resolution-based calculi. In: MFCS, volume 8635 of LNCS. Springer, pp 81-93 · Zbl 1426.68283 |
| [7] | Beyersdorff O, Janota M, Lonsing F, Seidl M (2021) Quantified Boolean formulas. In: Handbook of satisfiability, 2nd edn. Frontiers in artificial intelligence and applications. IOS Press |
| [8] | Biere A, Lonsing F, Seidl M (2011) Blocked clause elimination for QBF. In: CADE, volume 6803 of LNCS. Springer, pp 101-115 · Zbl 1341.68181 |
| [9] | Bloem R, Braud-Santoni N, Hadzic V, Egly U, Lonsing F, Seidl M (2018)Expansion-based QBF solving without recursion. In: FMCAD. IEEE, pp 1-10 |
| [10] | Bloem R, Könighofer R, Seidl M (2014) SAT-based synthesis methods for safety specs. In: VMCAI, volume 8318 of LNCS. Springer, pp 1-20 · Zbl 1428.68040 |
| [11] | Bogaerts B, Janhunen T, Tasharrofi S (2016) SAT-to-SAT in QBFEval 2016. In: QBF workshop, volume 1719 of CEUR workshop proceedings. CEUR-WS.org, pp 63-70 |
| [12] | Bogaerts B, Janhunen T, Tasharrofi S (2016) Solving QBF instances with nested SAT solvers. In: Beyond NP, volume WS-16-05 of AAAI Workshops. AAAI Press · Zbl 1379.68044 |
| [13] | Bubeck U, Kleine Büning H (2007) Bounded universal expansion for preprocessing QBF. In: SAT, volume 4501 of LNCS. Springer, pp 244-257 · Zbl 1214.68331 |
| [14] | Charwat G, Woltran S (2016) Dynamic programming-based QBF solving. In: QBF workshop, volume 1719 of CEUR workshop proceedings. CEUR-WS.org, pp 27-40 |
| [15] | Cheng C-H, Hamza Y, Ruess H (2016) Structural synthesis for GXW specifications. In: CAV, volume 9779 of LNCS. Springer, pp 95-117 · Zbl 1411.68059 |
| [16] | Cheng C-H, Lee EA, Ruess H (2017) autoCode4: structural controller synthesis. In TACAS, volume 10205 of LNCS. Springer, pp 398-404 |
| [17] | Clarke, EM; Grumberg, O.; Jha, S.; Yuan, L.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J ACM, 50, 5, 752-794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643 |
| [18] | Dershowitz N, Hanna Z, Katz J (2005) Bounded model checking with QBF. In: SAT, volume 3569 of LNCS. Springer, pp 408-414 · Zbl 1128.68366 |
| [19] | Egly, U.; Kronegger, M.; Lonsing, F.; Pfandler, A., Conformant planning as a case study of incremental QBF solving, Ann Math Artif Intell, 80, 1, 21-45 (2017) · Zbl 1409.68253 · doi:10.1007/s10472-016-9501-2 |
| [20] | Faymonville P, Finkbeiner B, Rabe MN, Tentrup L (2017) Encodings of bounded synthesis. In: TACAS, volume 10205 of LNCS. Springer, pp 354-370 · Zbl 1452.68118 |
| [21] | Bernd, F.; Leander, T., Detecting unrealizability of distributed fault-tolerant systems, Logic Methods Comput Sci, 11, 3, 1-31 (2015) · Zbl 1448.03018 |
| [22] | Gascón A, Tiwari A (2014) A synthesized algorithm for interactive consistency. In: NASA formal methods, volume 8430 of LNCS. Springer, pp 270-284 |
| [23] | Giunchiglia E, Marin P, Narizzano M (2009) Reasoning with quantified Boolean formulas. In: Handbook of satisfiability, volume 185 of FAIA. IOS Press, pp 761-780 |
| [24] | Giunchiglia E, Marin P, Narizzano M (2010) sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning. In: SAT, volume 6175 of LNCS. Springer, pp 85-98 · Zbl 1306.68157 |
| [25] | Heule, M.; Järvisalo, M.; Lonsing, F.; Seidl, M.; Biere, A., Clause elimination for SAT and QSAT, JAIR, 53, 127-168 (2015) · Zbl 1336.68231 · doi:10.1613/jair.4694 |
| [26] | Heyman T, Smith D, Mahajan Y, Leong L, Abu-Haimed H (2014) Dominant controllability check using QBF-solver and netlist optimizer. In: SAT, volume 8561 of LNCS. Springer, pp 227-242 · Zbl 1423.68450 |
| [27] | Janota, M., Towards generalization in QBF solving via machine learning (2018), In AAAI: AAAI Press, In AAAI |
| [28] | Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E., Solving QBF with counterexample guided refinement, Artif Intell, 234, 1-25 (2016) · Zbl 1351.68254 · doi:10.1016/j.artint.2016.01.004 |
| [29] | Janota M, Klieber W, Marques-Silva J, Clarke EM (2012) Solving QBF with counterexample guided refinement. In: SAT, volume 7317 of LNCS. Springer, pp 114-128 · Zbl 1273.68178 |
| [30] | Janota M, Marques-Silva J (2013) On propositional QBF expansions and Q-resolution. In: SAT, volume 7962 of LNCS. Springer, pp 67-82 · Zbl 1390.03017 |
| [31] | Janota, M.; Marques-Silva, J., Expansion-based QBF solving versus Q-resolution, Theor Comput Sci, 577, 25-42 (2015) · Zbl 1309.68168 · doi:10.1016/j.tcs.2015.01.048 |
| [32] | Janota M, Marques-Silva J (2015) Solving QBF by clause selection. In: IJCAI. AAAI Press, pp 325-331 |
| [33] | Janota M, Silva JPM (2011) Abstraction-based algorithm for 2QBF. In: SAT, volume 6695 of LNCS. Springer, pp 230-244 · Zbl 1330.68115 |
| [34] | Büning HK, Bubeck U (2009) Theory of quantified Boolean formulas. In: Handbook of satisfiability, volume 185 of FAIA. IOS Press, pp 735-760 |
| [35] | Büning, HK; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inf Comput, 117, 1, 12-18 (1995) · Zbl 0828.68045 · doi:10.1006/inco.1995.1025 |
| [36] | Klieber W, Sapra S, Gao S, Clarke EM (2010) A non-prenex, non-clausal QBF Solver with game-state learning. In: SAT, volume 6175 of LNCS. Springer, pp 128-142 · Zbl 1306.68161 |
| [37] | Letz R (2002) Lemma and model caching in decision procedures for quantified Boolean formulas. In: TABLEAUX, volume 2381 of LNCS. Springer, pp 160-175 · Zbl 1015.68173 |
| [38] | Lonsing F, Egly U (2017) DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: CADE, volume 10395 of LNCS. Springer, pp 371-384 · Zbl 1494.68288 |
| [39] | Lonsing F, Egly U (2018) Evaluating QBF solvers: quantifier alternations matter. In: CP, volume 11008 of LNCS. Springer, pp 276-294 |
| [40] | Lonsing F, Egly U (2019) Qratpre+: effective QBF preprocessing via strong redundancy properties. In: SAT, volume 11628 of LNCS. Springer, pp 203-210 · Zbl 1441.68229 |
| [41] | Peitl T, Slivovsky F, Szeider S (2017) Dependency Learning for QBF. In: SAT, volume 10491 of LNCS. Springer, pp 298-313 · Zbl 1478.68330 |
| [42] | Rabe MN, Tentrup L (2015) CAQE: a certifying QBF solver. In: FMCAD. IEEE, pp 136-143 |
| [43] | Ranjan DP, Tang D, Malik S (2004) A comparative study of 2QBF algorithms. In: SAT |
| [44] | Rintanen J (2007) Asymptotically optimal encodings of conformant planning in QBF. In: AAAI. AAAI Press, pp 1045-1050 |
| [45] | Shukla A, Biere A, Pulina L, Seidl M (2019) A survey on applications of quantified Boolean formulas. In: ICTAI. IEEE, pp 78-84 |
| [46] | Tentrup L (2016) Non-prenex QBF solving using abstraction. In: SAT, volume 9710 of LNCS. Springer, pp 393-401 · Zbl 1475.68224 |
| [47] | Tentrup L (2017) On expansion and resolution in CEGAR based QBF solving. In: CAV, volume 10427 of LNCS. Springer, pp 475-494 · Zbl 1494.68293 |
| [48] | Tu K-H, Hsu T-C, Jiang J-HR (2015) QELL: QBF reasoning with extended clause learning and levelized SAT solving. In: SAT, volume 9340 of LNCS. Springer, pp 343-359 · Zbl 1471.68263 |
| [49] | Vizel, Y.; Weissenbacher, G.; Malik, S., Boolean satisfiability solvers and their applications in model checking, Proc IEEE, 103, 11, 2021-2035 (2015) · doi:10.1109/JPROC.2015.2455034 |
| [50] | Wimmer R, Reimer S, Marin P, Becker B (2017) Hqspre—an effective preprocessor for QBF and DQBF. In: TACAS, volume 10205 of LNCS, pp 373-390 |
| [51] | Zhang L, Malik S (2002) Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: CP, volume 2470 of LNCS. Springer, pp 200-215 |
| [52] | Zhang W (2014) QBF encoding of temporal properties and QBF-based verification. In: IJCAR, volume 8562 of LNCS. Springer, pp 224-239 · Zbl 1423.68296 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
