Avoiding Tests for Subsumption

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Automated Reasoning

Useful equivalence-preserving operations based on antilinks are described. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. Those anti-links that directly indicate the presence of subsumed paths are characterized. These operations are useful for prime implicant/implicate algorithms because most of the computational effort in computing the prime implicants and prime implicates of a propositional formula is spent on subsumption checks. The problem of removing all subsumed paths in an NNF formula is shown to be NP-hard, even though such formulas may be small relative to the size of their path sets. The general problem of determining whether a pair of subsumed paths is associated with an arbitrary anti-link is shown to be NP-complete. Further reductions of subsumption checks are shown to be available when strictly put-e full blocks are present. The effectiveness of operations based on anti-links and strictly pure full blocks is examined with respect to some benchmark examples from the literature.