You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

An Extension of Deficiency and Minimal Unsatisfiability of Quantified Boolean Formulas


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.