Abstract
Many solvers have been designed for \(\mathcal{QBF}\)s, the validity problem for Quantified Boolean Formulas for the past few years. In this paper, we describe a new branching heuristics whose purpose is to promote renamable Horn formulas. This heuristics is based on Hébrard’s algorithm for the recognition of such formulas. We present some experimental results obtained by our qbf solver Qbfl with the new branching heuristics and show how its performances are improved.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving advanced reasoning tasks using quantified boolean formulas. In: AAAI 2000, Austin (USA), pp. 417–422 (2000)
Fargier, H., Lang, J., Marquis, P.: Propositional Logic and One-stage Decision Making. In: KR 2000, Breckenridge (CO), pp. 445–456 (2000)
Besnard, P., Schaub, T., Tompits, H., Woltran, S.: Paraconsistent Reasoning via Quantified Boolean Formulas, I: Axiomatising Signed Systems. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 320–331. Springer, Heidelberg (2002)
Rintanen, J.: Constructing Conditional Plans by a Theorem-Prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)
Pan, G., Sattler, U., Vardi, M.Y.: BDD-Based Decision Procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 16–30. Springer, Heidelberg (2002)
Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to Evaluate Quantified Boolean Formulae. In: AAAI 1998, Madison (USA), pp. 262–267 (1998)
Rintanen, J.: Improvements to the Evaluation of Quantified Boolean Formulae. In: IJCAI 1999, Stockholm (Sweden), pp. 1192–1197 (1999)
Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate quantified boolean formula. In: AAAI 2000, Austin (USA), pp. 285–290 (2000)
Rintanen, J.: Partial implicit unfolding in the Davis-Putnam procedure for Quantified Boolean Formulae. In: QBF 2001, Siena (Italy), pp. 84–93 (2001)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Logic Satisfiability. In: IJCAI 2001, Seattle (USA), pp. 275–281 (2001)
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, p. 160. Springer, Heidelberg (2002)
Zhang, L., Malik, S.: Towards a symetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (2002)
Pan, G., Vardi, M.: Optimizing a BDD-Based Modal Solver. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 75–89. Springer, Heidelberg (2003)
Audemard, G., Saïs, L.: SAT based BDD solver for Quantified Boolean Formulas. In: ICTAI 2004, Boca Raton (USA), pp. 82–89 (2004)
Aspvall, B., Plass, M., Tarjan, R.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters 8, 121–123 (1979); Erratum: Information Processing Letters 14(4), 195 (1982)
Gent, I.P., Rowley, A.: Solving 2-CNF Quantified Boolean Formulae using Variable Assignment and Propagation. In: QBF 2002, Cincinnati (USA), pp. 17–25 (2002)
Kleine-Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified boolean formulas. Information and Computation 117, 12–18 (1995)
Hébrard, J.J.: A Linear Algorithm for Renaming a Set of Clauses as a Horn Set. Theoretical Computer Science 124, 343–350 (1994)
Jeroslow, R.J., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1, 167–188 (1990)
Freemann, J.W.: Improvement to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania (1995)
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)
Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. Automated Reasoning 24, 297–317 (2000)
Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
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
Coste-Marquis, S., Le Berre, D., Letombe, F. (2005). A Branching Heuristics for Quantified Renamable Horn Formulas. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_30
Download citation
DOI: https://doi.org/10.1007/11499107_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)