Abstract
We make use of the algebraic theory that has been used to study the complexity of constraint satisfaction problems, to investigate tractable quantified boolean formulas. We present a pair of results: the first is a new and simple algebraic proof of the tractability of quantified 2-satisfiability; the second is a purely algebraic characterization of models for quantified Horn formulas that were given by Kleine Büning, Subramani, and Zhao, and described proof-theoretically.
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
Aspvall, B., Plass, M.F., Tarjan, R.E.: A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Inf. Process. Lett. 8(3), 121–123 (1979)
Börner, F., Bulatov, A., Krokhin, A., Jeavons, P.: Quantified Constraints: Algorithms and Complexity. Computer Science Logic (2003)
Bulatov, A.: Combinatorial problems raised from 2-semilattices. Manuscript
Bulatov, A.A.: A Dichotomy Theorem for Constraints on a Three-Element Set. In: FOCS 2002 (2002)
Bulatov, A.: Malt’sev constraints are tractable. Technical report PRG-RR-02-05, Oxford University (2002)
Bulatov, A.A.: Tractable conservative Constraint Satisfaction Problems. LICS (2003)
Bulatov, A.A., Krokhin, A.A., Jeavons, P.: Constraint Satisfaction Problems and Finite Algebras. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 272. Springer, Heidelberg (2000)
Bulatov, A., Jeavons, P.: An Algebraic Approach to Multi-sorted Constraints. In: Proceedings of 9th International Conference on Principles and Practice of Constraint Programming (2003)
Bulatov, A., Jeavons, P.: Algebraic structures in combinatorial problems. Technical report MATH-AL-4-2001, Technische Universitat Dresden (2001)
Bulatov, A., Jeavons, P.: Tractable constraints closed under a binary operation. Technical report PRG-TR-12-00, Oxford University (2000)
Chen, H., Dalmau, V. (Smart) Look-Ahead Arc Consistency and the Pursuit of CSP Tractability. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 182–196. Springer, Heidelberg (2004)
Creignou, N., Khanna, S., Sudan, M.: Complexity Classifications of Boolean Constraint Satisfaction Problems. SIAM Monographs on Discrete Mathematics and Applications 7 (2001)
Dalmau, V., Pearson, J.: Set Functions and Width 1. Constraint Programming (1999)
del Val, A.: On 2SAT and Renamable Horn. In: AAAI 2000, Proceedings of the Seventeenth (U.S.) National Conference on Artificial Intelligence, Austin, Texas, pp. 279–284 (2000)
Gent, I., Rowley, A.: Solving 2-CNF Quantified Boolean Formulae using Variable Assignment and Propagation. APES Research Group Report APES-46-2002 (2002)
Jeavons, P.: On the Algebraic Structure of Combinatorial Problems. Theor. Comput. Sci. 200(1-2), 185–204 (1998)
Jeavons, P.G., Cohen, D.A., Cooper, M.: Constraints, Consistency and Closure. Artificial Intelligence 101(1-2), 251–265 (1998)
Jeavons, P., Cohen, D.A., Gyssens, M.: Closure properties of constraints. J. ACM 44(4), 527–548 (1997)
Karpinski, M., Büning, H.K., Schmitt, P.H.: On the Computational Complexity of Quantified Horn Clauses. CSL 1987, 129–137 (1987)
Büning, H.K., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas. Information and Computation 117(1), 12–18 (1995)
Büning, H.K., 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)
Schaefer, T.: The complexity of satisfiability problems. In: Proceedings of the 10th Annual Symposium on Theory of Computing, ACM, New York (1978)
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
Chen, H., Dalmau, V. (2005). Looking Algebraically at Tractable Quantified Boolean Formulas. 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_6
Download citation
DOI: https://doi.org/10.1007/11527695_6
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)