Random walks for selected boolean implication and equivalence problems

This paper is concerned with the design and analysis of a random walk algorithm for the 2CNF implication problem (2CNFI). In 2CNFI, we are given two 2CNF formulas f₁{phi_{1}} and f₂{phi_{2}} and the goal is to determine whether every assignment that satisfies f₁{phi_{1}} , also satisfies f₂{phi_{2}} . The implication problem is clearly coNP-complete for instances of kCNF, k ≥ 3; however, it can be solved in polynomial time, when k ≤ 2. The goal of this paper is to provide a Monte Carlo algorithm for 2CNFI with a bounded probability of error. The technique developed for 2CNFI is then extended to derive a randomized, polynomial time algorithm for the problem of checking whether a given 2CNF formula Nae-implies another 2CNF formula.