AAAI Conference 1999 Conference Paper
Distance-SAT: Complexity and Algorithms
- Olivier Bailleux
- Pierre Marquis
- CRIL
- Université d'Artois
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.