Abstract
We propose in this article a unified framework for certificate and compilation for QBF. We provide a search-based algorithm to compute a certificate for the validity of a QBF and a search-based algorithm to compile a valid QBF in our unified framework.
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
Preview
Unable to display preview. Download preview PDF.
References
Ayari, A., Basin, D.: Qubos: Deciding quantified boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 187–201. Springer, Heidelberg (2002)
Benedetti, M.: Evaluating QBFs via Symbolic Skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 285–300. Springer, Heidelberg (2005)
Benedetti, M.: Extracting certificates from quantified boolean formulas. In: Proceedings of 9th International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 47–53 (2005)
Benedetti, M.: skizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 369–376. Springer, Heidelberg (2005)
Benedetti, M., Mangassarian, H.: Experience and perspectives in qbf-based formal verification. Journal on Satisfiability, Boolean Modeling and Computation (to appear, 2008)
Biere, A.: Resolve and expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Bordeaux, L.: Boolean and interval propagation for quantified constraints. In: First International Workshop on Quantification in Constraint Programming (2005)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Büning, H.K., Karpinski, M., Flögel, A.: Resolution for quantified boolean formulas. Information and Computation 117(1), 12–18 (1995)
Büning, H.K., Subramani, K., Zhao, X.: Boolean functions as models for quantified boolean formulas. Journal of Automated Reasoning 39(1), 49–75 (2007)
Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning 28(2), 101–142 (2002)
Coste-Marquis, S., Le Berre, D., Letombe, F., Marquis, P.: Propositional fragments for knowledge compilation and quantified boolean formulae. In: Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2005), pp. 288–293 (2005)
Coste-Marquis, S., Fargier, H., Lang, J., Le Berre, D., Marquis, P.: Representing policies for quantified boolean formulae. In: Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR 2006), pp. 286–296 (2006)
Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research 17, 229–264 (2002)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communication of the ACM 5 (1962)
Fargier, H., Marquis, P.: On the use of partially ordered decision graphs in knowledge compilation and quantified boolean formulae. In: AAAI (2006)
Garey, M.R., Johnson, D.S.: Computers and Intractability. A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1990)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified boolean formulas. Journal of Artificial Intelligence Research 26, 371–416 (2006)
Bacchus, F., Samulowitz, H.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005)
Jussila, T., Biere, A., Sinz, C., Kröning, D., Wintersteiger, C.: 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)
Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF Solving. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. SAT 2008, pp. 196–210. Springer, Heidelberg (2008)
Pan, G., Vardi, M.Y.: Symbolic Decision Procedures for QBF. In: International Conference on Principles and Practice of Constraint Programming (2004)
Plaisted, D.A., Biere, A., Zhu, Y.: A satisfiability procedure for quantified Boolean formulae. Discrete Applied Mathematics 130, 291–328 (2003)
Rintanen, J.: Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)
Stéphan, I.: Finding models for quantified boolean formulae. In: First International Workshop on Quantification in Constraint Programming (2005)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125. Consultants Bureau, New York (1970)
Yu, Y., Malik, S.: Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In: Proceedings of the 2005 conference on Asia South Pacific design automation (ASP-DAC 2005), pp. 1047–1051 (2005)
Zhang, L.: Solving QBF with combined conjunctive and disjunctive normal form. In: National Conference on Artificial Intelligence (AAAI 2006) (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stéphan, I., Da Mota, B. (2008). A Unified Framework for Certificate and Compilation for QBF. In: Ramanujam, R., Sarukkai, S. (eds) Logic and Its Applications. ICLA 2009. Lecture Notes in Computer Science(), vol 5378. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92701-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-92701-3_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92700-6
Online ISBN: 978-3-540-92701-3
eBook Packages: Computer ScienceComputer Science (R0)