Distance-SAT: Complexity and Algorithms

In many AI fields, the problem of finding out a solution which is as close as possible to a given configuration has to be faced. This paper addresses this problem in a propositional framework. The decision problem Distance-SAT that consists in determining whether a propositional CNF formula admits a model that disagrees with a given partial interpretation on at most d variables, is introduced. The complexity of Distance-SAT is investigated. Like its restriction SAT, Distance-SAT is NP-complete. However, Distance-SAT is shown somewhat more difficult than SAT, in the sense that the fragments for which SAT is tractable are not necessarily fragments for which Distance-SAT is tractable. Two algorithms based on the well-known Davis/Putnam search procedure are presented so as to solve Distance-SAT. Their empirical evaluation enables deriving firm conclusions about their respective performance, and to relate the difficulty of Distance-SAT with the difficulty of SAT from the practical side.