Distance-SAT: Complexity and Algorithms

In many AIfields, the problem of findingout a solution which is as closeas possibleto a givenconfiguration has to be faced. This paper addressesthis problem in a propositional framework. Thedecision problem DISTANCE-SAT that consists in determiningwhethera propositional CNF formulaadmitsa modelthat disagreeswitha givenpartial interpretationonat mostd variables, is introduced. Thecomplexity of DISTANCE- SAT andof severalrestrictionsof it areidentified. Two algorithms based on the well-knownDavis/Putnam searchprocedure are presented so as to solveDISTANCE- SAT. Theirempiricalevaluationenablesderivingfirm conclusions abouttheir respectiveperformances, and to relate the difficulty of DISTANCE-SAT withthe difficultyof SAT from the practical side.

Authors

• Olivier Bailleux
• Pierre Marquis Univ. Artois, CNRS, CRIL, Lens, France Institut Universitaire de France
• CRIL
• Université d'Artois

Keywords

No keywords are indexed for this paper.