publication . Other literature type . Article . 1979

A linear-time algorithm for testing the truth of certain quantified boolean formulas

Bengt Aspvall; Michael F. Plass; Robert Endre Tarjan;
  • Published: 01 Mar 1979
  • Publisher: Elsevier BV
Abstract
Let F = Qlxr Qzxz l ** Qnx, C be a quantified Boolean formula with no free variables, where each Qi is either 3 or t, and C is in conjunctive normal form. That is, C is a conjunction of clauses, each clause is a disjunction of literals, and each literal is either a variable, xi, or the negation of a variable, Zi (1 < i f n). We shall use Ui to denote a literal equal to either Xi or Fi. The evaluation problem for quantified Boolean formulas is to determine whether such a formula F is true. The evaluation problem is complete in polynomial space [6], even if C is restricted to contain at most three literals per clause. The satisfiability problem, the special case i...
Subjects
free text keywords: Combinatorics, Mathematics, Conjunctive normal form, Boolean satisfiability problem, Algorithm, Product term, Maximum satisfiability problem, 2-satisfiability, Discrete mathematics, Boolean expression, Karp–Lipton theorem, True quantified Boolean formula
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue