Abstract
Deciding the satisfiability of a Quantified Boolean Formula (QBF) is an important research issue in Artificial Intelligence. Many reasoning tasks involving planning [1], abduction, reasoning about knowledge, non monotonic reasoning [2], can be directly mapped into the problem of deciding the satisfiability of a QBF. In this paper we present QuBE, a system for deciding QBFs satisfiability.
We start our presentation in § 2 with some terminology and definitions necessary for the rest of the paper. In § 3 we present a high level description of QuBE’s basic algorithm. QuBE’s available options are described in § 4. We end our presentation in § 5 with some experimental results showing QuBE effectiveness in comparison with other systems. QuBE, and more information about QuBE, are available at www.mrg.dist.unige.it/star/qube.
We wish to thank Marco Cadoli, Rainer Feldmann, Theodor Lettman, Jussi Rintanen, Marco Schaerf and Stefan Schamberger for providing us with their systems and helping us to figure them out during our experimental analisys. This work has been partially supported by ASI and MURST.
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
Jussi Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323–352, 1999.
U. Egly, T. Eiter, H. Tompits, and S. Woltran. Solving advanced reasoning tasks using quantified boolean formulas. In Proc. AAAI, 2000.
D.A. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.
M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning, 2000. To appear. Reprinted in [13].
Jussi T. Rintanen. Improvements to the evaluation of quantified boolean formulae. In Dean Thomas, editor, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99-Vol2), pages 1192–1197, S.F., July 31-August 6 1999. Morgan Kaufmann Publishers.
R. Feldmann, B. Monien, and S. Schamberger. A distributed algorithm to evaluate quantified boolean formulae. In Proc. AAAI, 2000.
Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Back jumping for quantified boolean logic satisfiability. In Proc. of the International Joint Conference on Artificial Intelligence (IJCAI’2001), 2001.
M. Böhm and E Speckenmeyer. A fast parallel SAT-solver-efficient workload balancing. Annals of Mathematics and Artificial Intelligence, 17:381–400, 1996.
Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167–187, 1990.
Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 366–371, San Francisco, August 23-29 1997. Morgan Kaufmann Publishers.
Kleine-Büning, H. and Karpinski, M. and Flögel, A. Resolution for quantified boolean formulas. Information and computation, 117(1):12–18, 1995.
Ian Gent and Toby Walsh. Beyond NP: the QSAT phase transition. In Proc. AAAI, pages 648–653, 1999.
.Ian P. Gent, Hans Van Maaren, and Toby Walsh, editors. SAT2000. Highlights Of Satisfiability Research in the Year 2000. IOS Press, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giunchiglia, E., Narizzano, M., Tacchella, A. (2001). QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_27
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive