Abstract
Modern solvers for quantified Boolean formulas (QBF) not only decide the satisfiability of a formula, but also return a set of Skolem functions representing a model for a true QBF. Unfortunately, in combination with a preprocessor this ability is lost for many preprocessing techniques. A preprocessor rewrites the input formula to an equi-satisfiable formula which is often easier to solve than the original formula. Then the Skolem functions returned by the solver represent a solution for the preprocessed formula, but not necessarily for the original encoding.
Our solution to this problem is to combine Skolem functions obtained from a \(\mathsf {QRAT}\) trace as produced by the widely-used preprocessor Bloqqer with Skolem functions for the preprocessed formula. This approach is agnostic of the concrete rewritings performed by the preprocessor and allows the combination of Bloqqer with any Skolem function producing solver, hence realizing a smooth integration into the solving tool chain.
This work has been supported by the Austrian Science Fund (FWF) under projects W1255-N23 and S11408-N23, and by the National Science Foundation (NSF) under grant number CCF-1618574.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In the \(\mathsf {QRAT}\) format, clause deletion lines start with “d”.
References
Kleine Büning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Handbook of Satisfiability, pp. 735–760. IOS Press (2009)
Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. JSAT 5(1–4), 133–191 (2008)
Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1–20. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_1
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, Cham (2014). doi:10.1007/978-3-319-13770-4_11
Balabanov, V., Jiang, J.R., Scholl, C.: Skolem functions computation for CEGAR based QBF solvers. In: QBF (2015)
Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375–392. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_23
Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Form. Methods Syst. Des. 41(1), 45–65 (2012)
Benedetti, M.: Extracting certificates from quantified Boolean formulas. In: IJCAI, pp. 47–53. Professional Book Center (2005)
Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFs: a comparison of state-of-the-art tools. AI Commun. 22(4), 191–210 (2009)
Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430–435. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_33
Jussila, T., Biere, A., Sinz, C., Kröning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201–214. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72788-0_21
Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97–125 (2017)
Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: IJCAI/AAAI, pp. 546–553 (2011)
Van Gelder, A.: Certificate extraction from variable-elimination QBF preprocessors. In: QBF, pp. 35–39 (2013)
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)
Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified Boolean formulas. In: Handbook of Satisfiability, pp. 761–780. IOS Press (2009)
Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: FMCAD, pp. 136–143 (2015)
Lonsing, F., Seidl, M., Van Gelder, A.: The QBF gallery: behind the scenes. Artif. Intell. 237, 92–114 (2016)
Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows. Fundam. Inform. 149(1–2), 133–158 (2016)
Janota, M., Grigore, R., Marques-Silva, J.: On QBF proofs and preprocessing. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 473–489. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_32
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). doi:10.1007/978-3-642-22438-6_10
Lonsing, F., Egly, U.: DepQBF: an incremental QBF solver based on clause groups. CoRR abs/1502.02484 (2015)
Acknowledgements
We would like to thank Luca Pulina for providing us with the list of satisfiable instances of the QBF Eval 2016.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Fazekas, K., Heule, M.J.H., Seidl, M., Biere, A. (2017). Skolem Function Continuation for Quantified Boolean Formulas. In: Gabmeyer, S., Johnsen, E. (eds) Tests and Proofs. TAP 2017. Lecture Notes in Computer Science(), vol 10375. Springer, Cham. https://doi.org/10.1007/978-3-319-61467-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-61467-0_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-61466-3
Online ISBN: 978-3-319-61467-0
eBook Packages: Computer ScienceComputer Science (R0)