Abstract
We extend quantified 2-CNF formulas by also allowing literals over free variables which are exempt from the 2-CNF restriction. That means we consider quantified CNF formulas with clauses that contain at most two bound literals and an arbitrary number of free literals. We show that these \({\it Q2-CNF}^{b}\) formulas can be transformed in polynomial time into purely existentially quantified CNF formulas in which the bound literals are in 2-HORN (∃ 2 − HORN b).
Our result still holds if we allow Henkin-style quantifiers with explicit dependencies. In general, dependency quantified Boolean formulas (\({\it DQBF}\)) are assumed to be more succinct at the price of a higher complexity. This paper shows that \({\it DQ2-CNF}^{b}\) has a similar expressive power and complexity as ∃ 2 − HORN b. In the special case that the 2-CNF restriction is also applied to the free variables (\({\it DQ2-CNF}^{*}\)), the satisfiability can be decided in linear time.
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
Aanderaa, S., Börger, E.: The Horn Complexity of Boolean Functions and Cook’s Problem. In: Proc. 5th Scandinavian Logic Symposium 1979, pp. 231–256. Aalborg University Press (1979)
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)
Ayari, A., Basin, D.: QUBOS: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 187–201. Springer, Heidelberg (2002)
Babai, L., Fortnow, L., Lund, C.: Non-Deterministic Exponential Time has Two-Prover Interactive Protocols. Journal Computational Complexity 1(1), 3–40 (1991)
Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Bubeck, U., Kleine Büning, H.: Dependency Quantified Horn Formulas: Models and Complexity. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 198–211. Springer, Heidelberg (2006)
Bubeck, U., Kleine Büning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244–257. Springer, Heidelberg (2007)
Bubeck, U., Kleine Büning, H.: A New 3-CNF Transformation by Parallel-Serial Graphs. Journal Information Processing Letters 109(7), 376–379 (2009)
Dershowitz, N., Hanna, Z., Katz, J.: Bounded Model Checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 408–414. Springer, Heidelberg (2005)
Dowling, W., Gallier, J.: Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. Journal of Logic Programming 1(3), 267–284 (1984)
Even, S., Itai, A., Shamir, A.: On the Complexity of Timetable and Multi-Commodity Flow Problems. SIAM Journal on Computing 5(4), 691–703 (1976)
Flögel, A., Karpinski, M., Kleine Büning, H.: Resolution for Quantified Boolean Formulas. Information and Computation 117(1), 12–18 (1995)
Itai, A., Makowsky, J.: On the Complexity of Herbrand’s Theorem. Technical Report 243, Technion, Haifa (1982)
Jussila, T., Biere, A.: Compressing BMC Encodings with QBF. Electronic Notes in Theoretical Computer Science 174(3), 45–56 (2007)
Kleine Büning, H., Zhao, X., Bubeck, U.: Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 391–397. Springer, Heidelberg (2009)
Liberatore, P.: Redundancy in Logic II: 2-CNF and Horn Propositional Formulae. Artificial Intelligence 172(2-3), 265–299 (2008)
Lonsing, F., Biere, A.: A Compact Representation for Syntactic Dependencies in QBFs. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 398–411. Springer, Heidelberg (2009)
Peterson, G., Reif, J., Azhar, S.: Lower Bounds for Multiplayer Non-Cooperative Games of Incomplete Information. Computers and Mathematics with Applications 41(7-8), 957–992 (2001)
Plaisted, D., Greenbaum, S.: A Structure-preserving Clause Form Translation. Journal of Symbolic Computation 2(3), 293–304 (1986)
Sabharwal, A., Ansotegui, C., Gomes, C., Hart, J., Selman, B.: QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 382–395. Springer, Heidelberg (2006)
Samer, M., Szeider, S.: Backdoor Sets of Quantified Boolean Formulas. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 230–243. Springer, Heidelberg (2007)
Tseitin, G.: On the Complexity of Derivation in Propositional Calculus. In: Silenko, A. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115–125 (1970)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bubeck, U., Kleine Büning, H. (2010). Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN. In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-14186-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14185-0
Online ISBN: 978-3-642-14186-7
eBook Packages: Computer ScienceComputer Science (R0)