Distance-SAT: Complexity and Algorithms

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Satisfiability

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.