Abstract
We present the framework [q]bfGen which allows the declarative specification of random models for generating SAT and QSAT formulas not necessarily in (prenex) conjunctive normal form. To this end, [q]bfGen realizes a generic formula generator which creates formula instances by interpreting the random model specification expressed in XML. Consequently, the implementation of specific random formula generators becomes obsolete, because our framework subsumes their functionality.
This work was partially funded by the Vienna Science and Technology Fund (WWTF) through project ICT10-018, by the Austrian Science Fund (FWF) under grant S11409-N23 and by the Agence Nationale de la Recherche under grant ANR-09-BLAN-0011-01.
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.
Similar content being viewed by others
References
qbfGen Project Site, http://fmv.jku.at/qbfgen/
Benedetti, M., Mangassarian, H.: QBF-Based Formal Verification: Experience and Perspectives. JSAT 5(1-4), 133–191 (2008)
Brummayer, R., Lonsing, F., Biere, A.: Automated Testing and Debugging of SAT and QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010)
Chen, H., Interian, Y.: A Model for Generating Random Quantified Boolean Formulas. In: Proc. of IJCAI 2005, pp. 66–71. Professional Book Center (2005)
Creignou, N., Daudé, H., Egly, U., Rossignol, R.: (1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 363–376. Springer, Heidelberg (2009)
Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing Different Prenexing Strategies for Quantified Boolean Formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 214–228. Springer, Heidelberg (2004)
Egly, U., Seidl, M., Woltran, S.: A solver for QBFs in negation normal form. Constraints 14(1), 38–79 (2009)
Gent, I., Walsh, T.: Beyond NP: The QSAT Phase Transition. In: Proc. of AAAI/IAAI 1999, pp. 648–653 (1999)
Gent, I.P., Walsh, T.: The SAT Phase Transition. In: Proc. of ECAI 1994, pp. 105–109 (1994)
Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 412–426. Springer, Heidelberg (2009)
Klieber, W., Sapra, S., Gao, S., Clarke, E.: A Non-Prenex, Non-Clausal QBF Solver with Game-State Learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128–142. Springer, Heidelberg (2010)
Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: 2+p-sat: Relation of typical-case complexity to the nature of the phase transition. Random Struct. Algorithms 15(3-4), 414–435 (1999)
Navarro, J., Voronkov, A.: Generation of Hard Non-Clausal Random Satisfiability Problems. In: Proc. AAAI/IAAI 2005, pp. 436–442 (2005)
Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT 7(2), 156–173 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Creignou, N., Egly, U., Seidl, M. (2012). A Framework for the Specification of Random SAT and QSAT Formulas. In: Brucker, A.D., Julliand, J. (eds) Tests and Proofs. TAP 2012. Lecture Notes in Computer Science, vol 7305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30473-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-30473-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30472-9
Online ISBN: 978-3-642-30473-6
eBook Packages: Computer ScienceComputer Science (R0)