6533b85bfe1ef96bd12bab23
RESEARCH PRODUCT
Some Computational Aspects of DISTANCE-SAT
Olivier BailleuxPierre Marquissubject
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI]Theoretical computer scienceComputational complexity theory0102 computer and information sciences02 engineering and technologyComputer Science::Computational Complexity01 natural sciences[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]#SATArtificial IntelligenceComputer Science::Logic in Computer ScienceDPLL algorithm0202 electrical engineering electronic engineering information engineeringComputingMilieux_MISCELLANEOUSMathematicsDecision problemFunction problemSatisfiabilityPropositional formulaTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESComputational Theory and Mathematics010201 computation theory & mathematics020201 artificial intelligence & image processingBoolean satisfiability problemAlgorithmSoftwaredescription
In many AI fields, one must face the problem of finding a solution that is as close as possible to a given configuration. This paper addresses this problem in a propositional framework. We introduce 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. 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 behaviors are compared with the ones offered by sat solvers on sat encodings of distance-sat instances. The empirical evaluation allows us to draw 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.
year | journal | country | edition | language |
---|---|---|---|---|
2007-01-10 |