Computational complexity of quantified Boolean formulas with fixed maximal deficiency

AbstractThe paper investigates the computational complexity of quantified Boolean formulas with fixed maximal deficiency. The satisfiability problem for quantified Boolean formulas with maximal deficiency 1 is shown to be solvable in polynomial time. For k≥1, it is shown that true formulas with fixed maximal deficiency k have models in which all Boolean functions can be represented as CNF formulas over at most 24k/3 universal variables. As a consequence, the satisfiability problem for QCNF formulas with fixed maximal deficiency is in NP and for fixed deficiency the minimal falsity problem is in DP. For two subclasses of quantified Boolean formulas with PSPACE-complete evaluation problem, QEHORN and QE2-CNF , we show that for fixed deficiency the minimal falsity problem can be decided in polynomial time