Model Theory and Complexity of Quantified Boolean Formulas
by
Xishun Zhao
Sun Yat-sen University
Coauthors: H. Kleine Büning

The paper is devoted to review some recent results on model theory and computation complexity of quantified Boolean formulas (QBF). The satisfiability problem for QBFs (QSAT) is PSACE-complete. While QSAT for QBFs with a fixed prefix type S_n or P_n corresponding the polynomial hierarchy in complexity theory. We investigate QCNFs (i.e., QBFs with matrix in conjunctive normal form (CNF)) with fixed deficiency. Here, the deficiency of a QCNF formula is defined as the difference between the number of clauses and the number of existential variables which are quantified by existential quantifier in the prefix. We show that QSAT for QCNFs with maximal deficiency 1 can be solved in polynomial time. In order to study QSAT for QCNFs with fixed deficiency k > 1, we introduce the notion of models for QBFs.

Let F = ∀x₁ ∃y₁ ∀x₂ ∃x₂ ...∀x_k ∃y_k f be a closed quantified Boolean formula. The formula is true if and only if there are Boolean functions f_i : {x₁, ..., x_i} → {0, 1} such that f[y₁/f₁(x₁), ..., y_k/f_k(x₁, ..., x_k)] is tautological. A sequence of Boolean functions M=(f₁, ..., f_k) is called a model for F, if the formula is true for these functions. Subsequently, we assume that the Boolean functions f_i are represented as propositional formulas.

We can show that the model checking problem of determining if a sequence of Boolean functions is a model of an give formula is co-NP-complete. Then, the size of model functions have a close relationship with the complexity of QSAT problem. If in a subclass B ⊆ QCNF, every true formula has a polynomial size model, then QSAT for B will be in S^P₂. Thus, for any polynomial p(n), there seems to be a truth formula F ∈ B such that its every model has size exceeding p(|F|). However, 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 2^4k/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 D^P. For two subclasses of quantified Boolean formulas with PSPACE-complete evaluation problem, QEHORN and QE2CNF, we show that for fixed deficiency the minimal falsity problem can be decided in polynomial time.

PDF

Date received: March 3, 2008