×

zbMATH — the first resource for mathematics

Solution validation and extraction for QBF preprocessing. (English) Zbl 1409.68258
Summary: In the context of reasoning on quantified Boolean formulas (QBFs), the extension of propositional logic with existential and universal quantifiers, it is beneficial to use preprocessing for solving QBF encodings of real-world problems. Preprocessing applies rewriting techniques that preserve (satisfiability) equivalence and that do not destroy the formula’s CNF structure. In many cases, preprocessing either solves a formula directly or modifies it such that information helpful to solvers becomes better visible and irrelevant information is hidden. The application of a preprocessor, however, prevented the extraction of proofs for the original formula in the past. Such proofs are required to independently validate the correctness of the preprocessor’s rewritings and the solver’s result as well as for the extraction of solutions in terms of Skolem functions. In particular for the important technique of universal expansion efficient proof checking and solution generation was not possible so far. This article presents a unified proof system with three simple rules based on quantified resolution asymmetric tautology (\(\mathsf {QRAT}\)). In combination with an extended version of universal reduction, we use this proof system to efficiently express current preprocessing techniques including universal expansion. Further, we develop an approach for extracting Skolem functions. We equip the preprocessor bloqqer with \(\mathsf {QRAT}\) proof logging and provide a proof checker for \(\mathsf {QRAT}\) proofs which is also able to extract Skolem functions.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ayari ,A., Basin, D.A.: QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2002), Springer, LNCS, vol. 2517, pp. 187-201 (2002) · Zbl 1019.68597
[2] Balabanov, V., Jiang, J.R.: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. In: Proceedings of the 23rd Conference on Computer Aided Verification (CAV 2011), Springer, LNCS, vol. 6806, pp. 149-164 (2011)
[3] Balabanov, V; Jiang, JR, Unified QBF certification and its applications, Formal Methods Syst. Design, 41, 45-65, (2012) · Zbl 1284.68516
[4] Balabanov, V., Jiang J.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter)models from long-distance resolution proofs. In: Proceedings of the 29th Conference on Artificial Intelligence (AAAI 2015), pp. 3694-3701. AAAI Press (2015)
[5] Benedetti, M.: Extracting certificates from quantified Boolean formulas. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI 2005), Professional Book Center, pp. 47-53 (2005)
[6] Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Proceedings of the 20th International Conference on Automated Deduction (CADE 2005), LNCS, vol. 3632, pp. 369-376. Springer, Berlin (2005) · Zbl 1135.68550
[7] Benedetti, M; Mangassarian, H, QBF-based formal verification: experience and perspectives, J. Satisf. Boolean Model. Comput., 5, 133-191, (2008) · Zbl 1172.68538
[8] Biere, A.: Resolve and expand. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), LNCS, vol. 3542, pp. 59-70. Springer, Berlin (2005) · Zbl 1122.68585
[9] Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013 (2013) · Zbl 1336.68231
[10] Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Proceedings of the 23th International Conference on Automated Deduction (CADE 2011), LNCS, vol. 6803, pp. 101-115. Springer, Berlin (2011) · Zbl 1341.68181
[11] Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), LNCS, vol. 8318, pp. 1-20. Springer, Berlin (2014) · Zbl 1428.68040
[12] Bubeck, U., Kleine Büning, H.: Bounded universal expansion for preprocessing QBF. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), LNCS, vol. 4501, pp. 244-257. Springer, Berlin (2007) · Zbl 1214.68331
[13] Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified Boolean formulae. In: Proceedings of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference, (AAAI 98/IAAI 98), pp. 262-267. AAAI Press/The MIT Press, Cambridge (1998) · Zbl 0979.68124
[14] Davis, M; Putnam, H, A computing procedure for quantification theory, J. ACM, 7, 201-215, (1960) · Zbl 0212.34203
[15] Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning. In: Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), LNCS, vol. 6175, pp. 85-98. Springer, Berlin (2010) · Zbl 1306.68157
[16] Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Design, Automation and Test in Europe Conference and Exposition (DATE 2003), IEEE, pp. 10886-10891 (2003)
[17] Heule, M., Järvisalo, M., Biere, A.: Covered clause elimination. In: Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013), EasyChair Proceedings in Computing, vol. 13, pp. 41-46 (2013) · Zbl 1284.68516
[18] Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Proceedings of the 17th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2014), IEEE, pp. 107-114 (2014)
[19] Heule, M., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Proceedings of the 7th Internatioanl Joint Conference on Automated Reasoning (IJCAR 2014), LNCS, vol. 8562, pp. 91-106. Springer, Berlin (2014) · Zbl 1409.68257
[20] Heule, M; Järvisalo, M; Lonsing, F; Seidl, M; Biere, A, Clause elimination for SAT and QSAT, J. Artif. Intel. Res., 53, 127-168, (2015) · Zbl 1336.68231
[21] Heule, M., Jr WAH, Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Proceedings of the 25th International Conference on Automated Deduction (CADE 2015), LNCS, vol. 9195, pp. 591-606. Springer, Berlin (2015) · Zbl 06515534
[22] Heule, M., Seidl, M., Biere, A.: Blocked literals are universal. In: Proceedings of the 7th Internatonal Symposium on NASA Formal Methods (NFM 2015), LNCS, vol. 9058, pp. 436-442. Springer, Berlin (2015)
[23] Heule, M.J.H., Järvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Proceedings 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010), LNCS, vol. 6397, pp. 357-371. Springer, Berlin (2010) · Zbl 1306.68144
[24] Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Proceedings of the 24th International Conference on Automated Deduction (CADE 2013), LNAI, vol. 7898, pp. 345-359. Springer, Berlin (2013) · Zbl 1381.68270
[25] Heule, M.J.H., Hunt, Jr W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), IEEE, pp. 181-188 (2013)
[26] Janota, M; Marques-Silva, J, Expansion-based QBF solving versus Q-resolution, Theor. Comput. Sci., 577, 25-42, (2015) · Zbl 1309.68168
[27] Janota, M., Grigore, R., Marques-Silva, J.: On Checking of Skolem-based Models of QBF. In: Proceedings of the International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (2012)
[28] Janota, M,. Grigore, R., Marques-Silva, J.: On QBF proofs and preprocessing. In: Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013), LNCS, vol. 8312, pp. 473-489. Springer, Berlin (2013) · Zbl 1407.68454
[29] Järvisalo, M., Heule, M.J.H., Biere, A. Inprocessing rules. In: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), LNCS, vol. 7364, pp. 355-370. Springer, Berlin (2012) · Zbl 1358.68256
[30] Jordan, C., Seidl, M.: The QBF Gallery 2014. http://qbf.satisfiability.org/gallery/ (2014)
[31] Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic sat solving with quantification. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), vol. 4121, pp. 54-60. Springer, Berlin (2006) · Zbl 1187.68550
[32] Jussila, T., Biere, A., Sinz, C., Kröning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Proceedings of the 7th International Conference Theory and Applications of Satisfiability Testing (SAT 2007), LNCS, vol. 4501, pp. 201-214. Springer, Berlin (2007) · Zbl 1214.68334
[33] Kleine Büning, H; Karpinski, M; Flögel, A, Resolution for quantified Boolean formulas, Inf. Comput., 117, 12-18, (1995) · Zbl 0828.68045
[34] Kleine Büning, H., Subramani, K., Zhao, X.: Boolean functions as models for quantified Boolean formulas. J. Autom. Reason. 39(1), 49-75 (2007) · Zbl 1126.03015
[35] Könighofer, R., Seidl, M.: Partial witnesses from preprocessed quantified boolean formulas. In: Proceedings of Design, Automation & Test in Europe Conference & Exhibition, (DATE 2014), IEEE, pp. 1-6 (2014)
[36] Lonsing, F; Biere, A, Depqbf: a dependency-aware QBF solver, J. Satisf. Boolean Model. Comput., 7, 71-76, (2010)
[37] Lonsing, F., Seidl, M., Van Gelder. A.: The QBF Gallery: Behind the Scenes. CoRR abs/1508.01045, http://arxiv.org/abs/1508.01045 (2013) · Zbl 1357.68209
[38] Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), , LNCS, vol. 9450, pp. 418-433. Springer, Berlin (2015) · Zbl 06528797
[39] Narizzano, M; Peschiera, C; Pulina, L; Tacchella, A, Evaluating and certifying QBFS: a comparison of state-of-the-art tools, AI Commun., 22, 191-210, (2009) · Zbl 1186.68440
[40] Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF—(tool presentation). In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), LNCS, vol. 7317, pp. 430-435. Springer, Berlin (2012) · Zbl 0828.68045
[41] Samulowitz, H., Davies, J., Bacchus F.: Preprocessing QBF. In: Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP 2006), LNCS, vol. 4204, pp. 514-529. Springer, Berlin (2006)
[42] Slivovsky, F; Szeider, S, Soundness of Q-resolution with dependency schemes, Theor. Comput. Sci., 612, 83-101, (2016) · Zbl 1332.68204
[43] Van Gelder, A.: Variable independence and resolution paths for quantified Boolean formulas. In: Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011), LNCS, vol 6876, pp. 789-803. Springer, Berlin (2011) · Zbl 1273.68188
[44] Van Gelder, A.: Certificate extraction from variable-elimination QBF preprocessors. In: Proceedings of the 1st International Workshop on Quantified Boolean Formulas (QBF 2013), pp. 35-39 (2013)
[45] Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), LNCS, vol. 8561, pp. 422-429. Springer, Berlin (2014) · Zbl 1423.68475
[46] Yu, Y., Malik, S.: Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In: Proceedings of the Conference on Asia South Pacific Design Automation, (ASP-DAC 2005), pp. 1047-1051. ACM Press, New York (2005) · Zbl 1284.68516
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.