Abstract
The QSAT problem is the quantified version of the satisfiability problem SAT. We study the phase transition associated with random QSAT instances. We focus on a certain subclass of closed quantified Boolean formulas that can be seen as quantified extended 2-CNF formulas. The evaluation problem for this class is coNP-complete. We carry out an advanced practical and theoretical study, which illuminates the influence of the different parameters used to define random quantified instances.
This work has been supported by EGIDE 10632SE, ÖAD Amadée 2/2006 and ACI NIM 202.
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
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters 8(3), 121–123 (1979)
Chen, H., Interian, Y.: A model for generating random quantified Boolean formulas. In: Proceedings of the 19th International joint Conference on Artificial Intelligence, IJCAI 2005, pp. 66–71 (2005)
Chvátal, V., Reed, B.: Mick gets some (the odds are on his side). In: Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, FOCS 1992, pp. 620–627 (1992)
Creignou, N., Daudé, H., Dubois, O.: Expected number of locally maximal solutions for random Boolean CSPs. In: Proceedings of the13th International Conference on Analysis of Algorithms, AofA 2007, Antibes, June 2007. DMTCS, pp. 507–516 (2007)
Creignou, N., Daudé, H., Egly, U.: Phase transition for random quantified XOR-formulas. Journal of Artificial Intelligence Research 19, 1–18 (2007)
Dubois, O., Boufkhad, Y.: A general upper bound for the satisfiability threshold of random r-SAT formulae. Journal of Algorithms 24(2), 395–420 (1997)
Flögel, A., Karpinski, M., Kleine Büning, H.: Subclasses of quantified Boolean formulas. In: Schönfeld, W., Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1990. LNCS, vol. 533, pp. 145–155. Springer, Heidelberg (1991)
Gent, I.P., Walsh, T.: Beyond NP: the QSAT phase transition. In: Proceedings of AAAI 1999 (1999)
Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 364–369. Springer, Heidelberg (2001)
Goerdt, A.: A threshold for unsatisfiability. Journal of of Computer and System Sciences 53(3), 469–486 (1996)
Interian, Y., Corvera, G., Selman, B., Williams, R.: Finding small unsatisfiable cores to prove unsatisfiability of QBFs. In: Proceedings of the 9th International Symposium on Artificial Intelligence and Mathematics (2006)
Temme, N.M.: Asymptotic estimates of Stirling numbers. Stud. appl. Math. 89, 223–243 (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Creignou, N., Daudé, H., Egly, U., Rossignol, R. (2008). New Results on the Phase Transition for Random Quantified Boolean Formulas. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)