Abstract
This paper is concerned with the minimal falsity problem MF for quantified Boolean formulas. A QCNF formula (i.e., with CNF-matrix) is called minimal false, if the formula is false and any proper subformula is true. It is shown that the minimal falsity problem is PSPACE-complete. Then the deficiency of a QCNF formula is defined as the difference between the number of clauses and the number of existentially quantified variables. For quantified Boolean formulas with deficiency one, MF is solvable in polynomial time.
Some previous results of this of paper has been presented in the Workshop on Theory and Application of Quantified Boolean Formulas [3].
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. Information Processing Letters 8, 121–123 (1979)
Davydov, G., Davydova, I., Kleine Büning, H.: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence 23, 229–245 (1998)
Ding, D., Kleine Büning, H., Zhao, X.: Minimal Falsity for QBF with Fixed Deficiency. In: Proceedings of the Workshop on Theory and Applications of Quantified Boolean Formulas, IJCAR 2001, Siena, pp. 21–28 (2001)
Fleischner, H., Kullmann, O., Szeider, S.: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable deficiency. Theoretical Computer Scicence 289, 503–516 (2002)
Kleine Büning, H.: On Some Subclasses of Minimal Unsatisfiable Formulas. Discrete Applied Mathematics 107, 83–98 (2000)
Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)
Kleine Büning, H., Zhao, X.: On the structure of some classes of minimal unsatisfiable formulas. Discrete Applied Mathematics 130(2), 185–207 (2003)
Kullmann, O.: An Application of Matroid Theory to the ASAT Problem, Electronic Colloquium on Computational Complexity, Report 18 (2000)
Kullmann, O.: Lean-sets: Generalizations of minimal unsatisfiable clause-sets. Discrete Applied Mathematics 130, 209–249 (2003)
Kullmann, O.: The Combinatorics of Conflicts between Clauses. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 426–440. Springer, Heidelberg (2004)
Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. Journal of Computer and System Science 37, 2–13 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Büning, H.K., Zhao, X. (2006). Minimal False Quantified Boolean Formulas. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_32
Download citation
DOI: https://doi.org/10.1007/11814948_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)