DISTANCE-SAT: complexity and algorithms

Abstract

In many AI elds, the problem of nding out a solution which is as close as possible to a given conguration 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 dis-agrees with a given partial interpretation on at most d variables, is introduced. The complexity of distance-sat and of several restrictions of it are identied. Two algorithms based on the well-known Davis/Putnam search procedure are presented so as to solve distance-sat. Their empirical evaluation enables deriving rm conclusions about their respective performances, and to relate the diculty of distance-sat with the di-culty of sat from the practical side.