Solving SAT Efficiently with Promises (<Special Issue>Special Issue on Selected Papers from LA Symposium)

概要

論文の詳細を見る
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 [7]. 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★e<1) satisfying assignments, we present a subexponential-time deterministic algorithm based on the inclusion-exclusion formula.
社団法人電子情報通信学会の論文
2003-02-01