*Olivier Bailleux and Pierre Marquis, CRIL, Université d'Artois*

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.