Abstract
2QBF is a special form \(\forall \varvec{x} \exists \varvec{y}.\phi \) of the quantified Boolean formula (QBF) restricted to only two quantification layers, where \(\phi \) is a quantifier-free formula. Despite its restricted form, it provides a framework for a wide range of applications, such as artificial intelligence, graph theory, synthesis, etc. In this work, we overview two main 2QBF challenges in terms of solving and certification. We contribute several improvements to existing solving approaches and study how the corresponding approaches affect certification. We further conduct an extensive experimental comparison on both competition and application benchmarks to demonstrate strengths of the proposed methodology.
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
Similar content being viewed by others
Notes
- 1.
All the tools, benchmarks, and experimental results can be found at
https://www.dropbox.com/s/xyfb2i9xl1pvrv3/sat16_tools_2qbf.zip?dl=0.
References
QBF Gallery 2014. http://qbf.satisfiability.org/gallery/
QBF solver evaluation portal. http://www.qbflib.org/qbfeval/
QDIMACS: Standard QBF input format. http://www.qbflib.org/qdimacs
Balabanov, V., Jiang, J.-H.R.: Unified QBF certification and its applications. Formal Meth. Syst. Des. 41, 45–65 (2012)
Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 369–376. Springer, Heidelberg (2005)
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)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: an efficient QBF solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 201–213. Springer, Heidelberg (2004)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified Boolean formulas. J. Artif. Intell. Res. (JAIR) 26, 371–416 (2006)
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012)
Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230–244. Springer, Heidelberg (2011)
Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings International Joint Conference on Artificial Intelligence (IJCAI), pp. 325–331 (2015)
Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver (system description). J. Satisfiability Boolean Model. Comput. 7, 71–76 (2010)
Marques-Silva, J.P., Sakallah, K.A.: Boolean satisfiability in electronic design automation. In: Proceednigs Design Automation Conference (DAC), pp. 675–680 (2000)
Mishchenko, A., Brayton, R.K., Feng, W., Greene, J.W.: Technology mapping into general programmable cells. In: Proceedings International Symposium on Field-Programmable Gate Arrays (FPGA), pp. 70–73 (2015)
Mneimneh, M., Sakallah, K.A.: Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 411–425. Springer, Heidelberg (2004)
Pigorsch, F., Scholl, C.: Exploiting structure in an AIG based QBF solver. In: Proceedings Design, Automation and Test in Europe (DATE), pp. 1596–1601 (2009)
Remshagen, A., Truemper, K.: An effective algorithm for the futile questioning problem. J. Autom. Reasoning 34(1), 31–47 (2005)
Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174–187. Springer, Heidelberg (2011)
Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic (1970)
Acknowledgments
This work was partly supported by NSF/NSA grant “Enhanced equivalence checking in cryptoanalytic applications” at University of California, Berkeley.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Balabanov, V., Jiang, JH.R., Scholl, C., Mishchenko, A., Brayton, R.K. (2016). 2QBF: Challenges and Solutions. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-40970-2_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40969-6
Online ISBN: 978-3-319-40970-2
eBook Packages: Computer ScienceComputer Science (R0)