Non-clausal Encoding of Feature Diagram for Automated Diagnosis

摘要

Automated support for finding unsatisfiable fragments is desirable to help removing deficiency in inconsistent feature diagrams. In encoding feature diagrams into propositional logic formulas, such a problem reduces to finding unsatisfiable cores. Standard algorithms work on clausal formulas, which looses the structural aspect of feature diagram. In this paper, we propose a new automated method, which employs a boolean constraint propagation algorithm for non-clausal formulas. The method can eliminate the problems in the previous approaches, where translation back and forth is required between feature diagram and clausal formulas.