Some Computational Aspects of distance-sat

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 which consists in determining whether a propositional formula admits a model that disagrees with a given partial interpretation on at most d variables, is introduced. The complexity of distance-sat and of several restrictions of it are identified. Two algorithms based on the well-known Davis/Logemann/Loveland search procedure for the satisfiability problem sat are presented so as to solve distance-sat for CNF formulas. Their computational behaviours are compared with the ones offered by sat solvers on sat encodings of distance-sat instances. The empirical evaluation allows for drawing firm conclusions about the respective performances of the algorithms, and to relate the difficulty of distance-sat with the difficulty of sat from the practical side.

• Type: Journal
• Year: 2006
• Where: JAR
• Authors: Olivier Bailleux, Pierre Marquis
• Keywords: Decision Problem, JAR 2006, Propositional Formula, Propositional Framework