An Extension of Deficiency and Minimal Unsatisfiability of Quantified Boolean Formulas

Hans Kleine Buening, Xishun Zhao

Abstract


The notion of minimal unsatisfiability and minimal falsity will be extended to non-clausal and non-prenex quantified Boolean formulas. For quantified Boolean formulas in negation normal form we generalize the notion of deficiency to the so-called cohesion, which is 1+ the difference between the number of occurrences of the conjunction symbol ∧ and the number of existential and free variables. Further, we show that all the complexity results with respect to minimal unsatisfiability or minimal falsity known for formulas with fixed deficiency can be adapted to formulas with fixed cohesion. For example, (1) the minimal unsatisfiability of propositional formulas with fixed cohesion is still solvable in polynomial time and, (2) the minimal falsity of quantified Boolean formulas with cohesion 1 is solvable in polynomial time.

Keywords


deficiency, cohesion, QBF, minimal unsatisfiability, minimal falsity

Full Text:

PDF

Refbacks

  • There are currently no refbacks.