Abstract
In this paper, quantified Horn formulas with free variables (QHORN *) are investigated. The main result is that any quantified Horn formula Φ of length |Φ| with free variables, |∀| universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent formula of length O(| ∀ | ·|Φ|) which contains only existential quantifiers. Moreover, it is shown that quantified Horn formulas with free variables have equivalence models where every existential quantifier is associated with a monotone Boolean function.
The results allow a simple representation of quantified Horn formulas as purely existentially quantified Horn formulas (∃ HORN *). An application described in the paper is to solve QHORN *-SAT in O(| ∀ | ·|Φ|) by using this transformation in combination with a linear-time satisfiability checker for propositional Horn formulas.
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.
Similar content being viewed by others
References
Aspvall, B., Plass, M., Tarjan, R.: A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Information Processing Letters 8(3), 121–123 (1979)
Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Proc. 16th Natl. Conf. on AI, AAAI 1998 (1998)
Dowling, W., Gallier, J.: Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. of Logic Programming 1(3), 267–284 (1984)
Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)
Kleine Büning, H., Subramani, K., Zhao, X.: On Boolean Models for Quantified Boolean Horn Formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 93–104. Springer, Heidelberg (2004)
Kleine Büning, H., Zhao, X.: Equivalence Models for Quantified Boolean Horn Formulas. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 224–234. Springer, Heidelberg (2005)
Le Berre, D., Narizzano, M., Simon, L., Tacchella, A.: The second QBF solvers comparative evaluation. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 376–392. Springer, Heidelberg (2005)
Letz, R.: Advances in Decision Procedures for Quantified Boolean Formulas. In: Proc. IJCAR 2001 Workshop on Theory and Applications of QBF (2001)
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, p. 362. 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
Bubeck, U., Büning, H.K., Zhao, X. (2005). Quantifier Rewriting and Equivalence Models for Quantified 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_29
Download citation
DOI: https://doi.org/10.1007/11499107_29
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)