Abstract
How can we find any satisfying assignment for a Boolean formula that has many satisfying assignments? There exists an obvious randomized algorithm for solving this problem: one can just pick an assignment at random and check the truth value of the formula for this assignment, this is iterated until a satisfying assignment occurs. Does there exist a polynomial-time deterministic algorithm that solves the same problem? This paper presents such an algorithm and shows that its worst-case running time is linear when input formulas are in k-CNF and a fraction of satisfying assignments is greater than a constant. This algorithm is almost the same as the algorithm proposed by Monien and Speckenmeyer in the early 1980s for less than 2n steps 3-SAT decision.Another result of this paper is that if a formula in k-CNF has many satisfying assignments, then there exists a short satisfying assignment, i.e. an assignment of truth values to a small number of variables. The proposed algorithm yields just such a short satisfying assignment. We also show that there exist formulas in general CNF having many satisfying assignments, that have no short satisfying assignments