×

zbMATH — the first resource for mathematics

Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API. (English) Zbl 06512573
Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-24317-7/pbk; 978-3-319-24318-4/pbk). Lecture Notes in Computer Science 9340, 191-198 (2015).
Summary: We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables and assumptions from the user, which facilitates the integration of DepQBF in other tools.
We present implementation details and, for the first time, report on experiments related to the computation of MUCs of QBFs using DepQBF’s novel clause group API.
For the entire collection see [Zbl 1323.68009].

MSC:
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Efficient generation of unsatisfiability proofs and cores in SAT. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 16–30. Springer, Heidelberg (2008) · Zbl 1182.68215 · doi:10.1007/978-3-540-89439-1_2
[2] Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013) · Zbl 1390.68587 · doi:10.1007/978-3-642-39071-5_23
[3] Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012) · Zbl 1248.68450
[4] Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. JSAT 5, 133–191 (2008) · Zbl 1172.68538
[5] Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 101–115. Springer, Heidelberg (2011) · Zbl 1341.68181 · doi:10.1007/978-3-642-22438-6_10
[6] Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. J. Autom. Reasoning 28(2), 101–142 (2002) · Zbl 1002.68165 · doi:10.1023/A:1015019416843
[7] Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 334–339. Springer, Heidelberg (2007) · Zbl 1214.68348 · doi:10.1007/978-3-540-72788-0_32
[8] Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36–41. Springer, Heidelberg (2006) · Zbl 1187.68538 · doi:10.1007/11814948_5
[9] Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37
[10] Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543–560 (2003) · Zbl 1271.68215 · doi:10.1016/S1571-0661(05)82542-3
[11] Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. In: Aranda-Corral, G.A., Calmet, J., Martín-Mateos, F.J. (eds.) AISC 2014. LNCS, vol. 8884, pp. 120–131. Springer, Heidelberg (2014) · Zbl 06400222 · doi:10.1007/978-3-319-13770-4_11
[12] Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/Term resolution and learning in the evaluation of quantified boolean formulas. J. Artif. Intell. Res. (JAIR) 26, 371–416 (2006) · Zbl 1183.68475
[13] Grégoire, É., Mazure, B., Piette, C.: On Approaches to Explaining Infeasibility of Sets of Boolean Clauses. In: ICTAI, pp. 74–83. IEEE Computer Society (2008) · doi:10.1109/ICTAI.2008.39
[14] Ignatiev, A., Janota, M., Marques-Silva, J.: Quantified maximum satisfiability. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 250–266. Springer, Heidelberg (2013) · Zbl 1390.68598 · doi:10.1007/978-3-642-39071-5_19
[15] Jussila, T., Biere, A.: Compressing BMC encodings with QBF. ENTCS 174(3), 45–56 (2007) · Zbl 1277.68136
[16] Kleine Büning, H., Zhao, X.: Minimal false quantified boolean formulas. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 339–352. Springer, Heidelberg (2006) · Zbl 1152.68449 · doi:10.1007/11814948_32
[17] Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed Up MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276–292. Springer, Heidelberg (2013) · Zbl 1390.68601 · doi:10.1007/978-3-642-39071-5_21
[18] Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, p. 160. Springer, Heidelberg (2002) · Zbl 1015.68173 · doi:10.1007/3-540-45616-3_12
[19] Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008) · Zbl 1154.68510 · doi:10.1007/s10817-007-9084-z
[20] Lonsing, F., Egly, U.: Incremental QBF solving. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 514–530. Springer, Heidelberg (2014) · Zbl 06461434 · doi:10.1007/978-3-319-10428-7_38
[21] Lonsing, F., Egly, U.: Incremental QBF solving by DepQBF. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 307–314. Springer, Heidelberg (2014) · Zbl 1434.68547 · doi:10.1007/978-3-662-44199-2_48
[22] Lonsing, F., Egly, U.: Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. CoRR abs/1502.02484 (2015). http://arxiv.org/abs/1502.02484
, SAT 2015 proceedings version (6-page tool paper) with appendix · Zbl 06512573
[23] Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Verification of Partial Designs using Incremental QBF Solving. In: Rosenstiel, W., Thiele, L. (eds.) DATE, pp. 623–628. IEEE (2012) · doi:10.1109/DATE.2012.6176547
[24] Marques-Silva, J.: Minimal unsatisfiability: models, algorithms and applications (Invited Paper). In: ISMVL, pp. 9–14. IEEE Computer Society (2010)
[25] Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159–173. Springer, Heidelberg (2011) · Zbl 1330.68273 · doi:10.1007/978-3-642-21581-0_14
[26] Miller, C., Marin, P., Becker, B.: Verification of partial designs using incremental QBF. AI Commun. 28(2), 283–307 (2015) · Zbl 1373.68382
[27] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC, pp. 530–535. ACM (2001)
[28] Nadel, A.: Boosting Minimal Unsatisfiable Core Extraction. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 221–229. IEEE (2010)
[29] Nadel, A., Ryvchin, V., Strichman, O.: Accelerated deletion-based extraction of minimal unsatisfiable cores. JSAT 9, 27–51 (2014)
[30] Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 206–218. Springer, Heidelberg (2014) · Zbl 1423.68464 · doi:10.1007/978-3-319-09284-3_16
[31] Yu, Y., Malik, S.: Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice. In: Tang, T. (ed.) ASP-DAC, pp. 1047–1051. ACM Press (2005) · doi:10.1145/1120725.1120821
[32] Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 200. Springer, Heidelberg (2002) · Zbl 05876498 · doi:10.1007/3-540-46135-3_14
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.