Sciweavers

JAR
2006

Some Computational Aspects of distance-sat

13 years 3 months ago
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.
Olivier Bailleux, Pierre Marquis
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JAR
Authors Olivier Bailleux, Pierre Marquis
Comments (0)