In this paper, we discuss a simple, Monte Carlo algorithm for the problem of checking whether a Quantified Boolean Formula (QBF) in Conjunctive Normal Form (CNF), with at most two literals per clause has a model. The term k-CNF is used to describe boolean formulas in CNF, with at most k literals per clause and the problem of checking whether a given k-CNF formula is satisfiable is called the k-SAT problem. A QBF is a boolean formula, accompanied by a quantifier string which imposes a linear ordering on the variables of that formula. The problem of finding a model for a QBF formula in CNF, with at at most k literals per clause is called the QkSAT problem. The QkSAT problem is PSPACE-complete, for k≥3. However, the Q2SAT problem can be decided in polynomial time; the graph-based procedure, discussed in [1], is the first such algorithm for this problem. This procedure requires the construction of a global implication graph, corresponding to the input formula and searching for certain paths in this graph. Hence the complete set of clauses must be part of the input. We propose an incremental, randomized approach for the Q2SAT problem that is essentially local in nature, in that the complete clausal set need not be provided at any time, in the presence of a verifier. We show that the randomized algorithm can be analyzed as a one-dimensional random walk, with one reflecting barrier and one absorbing barrier. On a Q2SAT instance with m clauses on n variables, our coin-flipping algorithm runs in time O(n2 · V(m, n)), where V(m, n) is the time required to verify that a given model satisfies the formula. Additionally, if the instance is satisfiable, the probability that our algorithm fails to find a model is less than one half. The design and analysis of a randomized algorithm for a problem, is important from both the theoretical and the practical perspectives. Randomized approaches tend to be simple and elegant, thereby making the process of checking correctness, effortless as well. The randomized approach discussed in this paper lays the groundwork for analyzing a number of problems related to 2CNF formulas and directed graphs. We remark that our work in this paper is the first randomized algorithm for a class of QBFs.
Quantified Boolean Formulas: Call the Plumber!