Abstract
During the recent years, the development of tools for deciding Quantified Boolean Formulas (QBFs) satisfiability has been accompanied by a steady supply of real-world instances, i.e., QBFs originated by translations from application domains such as formal verification and planning. QBFs from these domains showed to be challenging for current state-of-the-art QBF solvers, and, in order to tackle them, several techniques and even specialized solvers have been proposed. Among these techniques, there are (i) efficient detection and propagation of unit and monotone literals, (ii) branching heuristics that leverages the information extracted during the learning phase, and (iii) look-back techniques based on learning.
In this paper we discuss their implementation in our state-of-the-art solver QuBE, pointing out the non trivial issues that arised in the process. We show that all the techniques positively contribute to QuBE performances on average. In particular, we show that monotone literal fixing is the most important technique in order to improve capacity, followed by learning and the heuristics. The situation is reversed if we consider productivity. These and other observations are detailed in the body of the paper. For our analysis, we consider the formal verification and planning benchmarks from the 2003 QBF evaluation.
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
Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: 38th Design Automation Conference, DAC 2001 (2001)
Ayari, A., Basin, D.: Bounded model construction for monadic second-order logics. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 99–113. Springer, Heidelberg (2000)
Rintanen, J.: Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)
Castellini, C., Giunchiglia, E., Tacchella, A.: Improvements to SAT-based conformant planning. In: Proc. ECP (2001)
Mneimneh, M.N., 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)
Gent, I., Giunchiglia, E., Narizzano, M., Rowley, A., Tacchella, A.: Watched data structures for QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 25–36. Springer, Heidelberg (2004)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Monotone literals and learning in QBF reasoning. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 260–273. 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.: Learning for Quantified Boolean Logic Satisfiability. In: Proc. 18th National Conference on Artificial Intelligence (AAAI) (AAAI 2002), pp. 649–654 (2002)
Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design, ICCAD 2002 (2002)
Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002)
Copty, F., Fix, L., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 436. Springer, Heidelberg (2001)
Le Berre, D., Simon, L., Tacchella, A.: Challenges in the QBF arena: the SAT 2003 evaluation of QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 468–485. Springer, Heidelberg (2004)
Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Proc. AAAI (1998)
Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Proceedings of the 19th International Conference on Automated Deduction (2003)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (June 2001)
Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design, pp. 220–227 (November 1996)
Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI 1997/IAAI 1997), July 27–31, pp. 203–208. AAAI Press, Menlo Park (1997)
Gent, I.P., Rowley, A.G.D.: Solution learning and solution directed backjumping revisited. Technical Report APES-80-2004, APES Research Group (February 2004), Available from http://www.dcs.st-and.ac.uk/~apes/apesreports.html
Kleine-Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Information and computation 117(1), 12–18 (1995)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause-term resolution and learning in quantified Boolean logic satisfiability (2004) (submitted)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Logic Satisfiability. Artificial Intelligence 145, 99–120 (2003)
Rintanen, J.: Partial implicit unfolding in the Davis-Putnam procedure for Quantified Boolean Formulae. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 362–376. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giunchiglia, E., Narizzano, M., Tacchella, A. (2005). QBF Reasoning on Real-World Instances. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing. SAT 2004. Lecture Notes in Computer Science, vol 3542. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527695_9
Download citation
DOI: https://doi.org/10.1007/11527695_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27829-0
Online ISBN: 978-3-540-31580-3
eBook Packages: Computer ScienceComputer Science (R0)