Solving SAT Efficiently with Promises

Kazuo IWAMA, Akihiro MATSUURA

Summary :

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 (i) when p=n^c (-1 < c 0), the problem is NP-hard; and (ii) when p=log n/n, there exists a polynomial-time deterministic algorithm. The algorithm is based on the exponential-time algorithm recently presented by Schoning. It is also applied for coloring k-uniform hypergraphs. The other promise is the number of satisfying assignments. For a CNF formula having 2ⁿ/2^nε (0 ε < 1) satisfying assignments, we present a subexponential-time deterministic algorithm based on the inclusion-exclusion formula.

• Publication: IEICE TRANSACTIONS on Information Vol.E86-D No.2 pp.213-218
• Publication Date: 2003/02/01
• Type of Manuscript: Special Section PAPER (Special Issue on Selected Papers from LA Symposium)
• Category: Turing Machine, Recursive Functions

Authors

Kazuo IWAMA
Akihiro MATSUURA

Keyword

SAT,  CNF formula,  promise,  solution-density,  inclusion-exclusion