The complexity of the satisfiability problem for Krom formulas (Q800915)

A Krom formula is a formula of pure quantificational theory whose matrix is in conjunctive normal form with at most two disjuncts in each conjunct. The authors study the computational complexity of the satisfiability problem for Krom formulas. Their results are as follows: (1) Satisfiability is decidable in polynomial time for Krom formulas with prefix \(\forall \exists \forall\). Moreover, the unsatisfiable Krom formulas with prefix \(\forall \exists \forall\) form a class complete for nondeterministic log space. (2) Satisfiability for Krom formulas with prefix \(\exists^*\forall^*\exists^*\) is a complete problem for deterministic exponential time. But for each fixed k, satisfiability for Krom formulas with prefix \(\exists^*\forall^ k\exists^*\) is decidable in polynomial time. (3) Satisfiability for Krom formulas with prefix \(\exists^*\forall^*\) is a complete problem for polynomial space. (4) Satisfiability for monadic Krom formulas is complete for P.