Abstract
Trivial truth and backjumping are two optimization techniques that have been proposed for deciding quantified boolean formulas (QBFs) satisfiability. Both these techniques can greatly improve the overall performance of a QBF solver, but they are the expression of opposite philosophies. On one hand, trivial truth is a “look-ahead” policy: it is applied when descending the search tree to (try to) prune it. On the other hand, backjumping is a “look-back” policy: it is applied when backtracking to (try to) avoid useless explorations. Neither of these optimizations subsumes the other: it is easy to come up with examples in which trivial truth behaves much better than backjumping, and the other way around. In this paper we experimentally evaluate these two optimizations both on randomly generated and on real world test cases.
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
M. Cadoli, A. Giovanardi, and M. Schaerf. An algorithm to evaluate quantified boolean formulae. In Proc. of AAAI, 1998.
M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation. In Highlights of Satisfiability Research in the Year 2000. IOS Press, 2000.
E. Giunchiglia, M. Narizzano, and A. Tacchella. Backjumping for Quantified Boolean Logic Satisfiability. In Proc. of IJCAI, 2001. To appear.
E. Giunchiglia, M. Narizzano, and A. Tacchella. QuBE: a system for Deciding Quantified Boolean Formulas Satisfiability. In Proc. of IJCAR, 2001.
R. Feldmann, B. Monien, and S. Schamberger. A Distributed Algorithm to Evaluate Quantified Boolean Formulae. In Proc. of AAAI, 2000.
Ian Gent and Toby Walsh. Beyond NP: the QSAT phase transition. In Proc. of AAAI, pages 648–653, 1999.
J. T. Rintanen. Improvements to the Evaluation of Quantified Boolean Formulae. In Proc. of IJCAI, pages 1192–1197, 1999.
H. Kleine-Büning and M. Karpinski and A. Flögel. Resolution for quantified boolean formulas. Information and Computation, 117(1):12–18, 1995.
D.A. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.
E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proc. of IJCAR, LNCS. Springer Verlag, 2001. To appear.
M. Buro and H. Kleine-Büning. Report on a SAT competition. Technical Report 110, University of Paderborn, November 1992.
D. S. Moore and G. P. McCabe. Introduction to the Practice of Statistics. W. H. Freeman and Co., 1993.
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). An Analysis of Backjumping and Trivial Truth in Quantified Boolean Formulas Satisfiability. In: Esposito, F. (eds) AI*IA 2001: Advances in Artificial Intelligence. AI*IA 2001. Lecture Notes in Computer Science(), vol 2175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45411-X_13
Download citation
DOI: https://doi.org/10.1007/3-540-45411-X_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42601-1
Online ISBN: 978-3-540-45411-3
eBook Packages: Springer Book Archive