Solving SAT Efficiently with Promises

摘要

In this paper, we consider two types of promises for (k-)CNF formulas which can help to find a satisfying assignment of a given formula. The first promise is the Hamming distance between truth assignments. Namely, we know in advance that a k-CNF formula with n variables, if satisfiable, has a satisfying assignment with at most pn variables set to 1. Then we ask whether or not the formula is satisfiable. It is shown that for k ≧ 3 and (ⅰ) when p = n~c (-1 < c ≦ 0), the problem is NP-hard; and (ⅱ) when p = log n, there exists a polynomial-time deterministic algorithm. The algorithm is based on the exponential-time algorithm recently presented by Schoening, It is also applied for coloring k-uniform hypergraphs. The other promise is the number of satisfying assignments. For a CNF formula having 2~n/2~(n~ε) (0 ≦ ε < 1) satisfying assignments, we present a subexponential-time deterministic algorithm based on the inclusion-exclusion formula.