|
Abstract : |
Abstract. A variable in a propositional formula is called inadmissible (necessary) if it is false (true) in each satisfying variable assignment of the formula. We describe and compare three algorithms for the detection of the set of necessary and inadmissible variables of a formula using SAT methods: a basic solution that iteratively assigns true (false) to each variable and tests the resulting formula for satisability as well as two enhanced algorithms. The rst enhancement tries to avoid the costly SAT algorithm by reusing the results of previous satisability checks, while the second is designed to maximize the number of variables that can be classied without SAT checking by adequately directing the variable selection in previous runs of the SAT algorithm. Experiments with large propositional formulae generated for the analysis and veri-cation of a rule-based automotive product database demonstrate the eciency and usefulness of these algorithms. 1, |
