Avoiding Tests for Subsumption

Anavai Ramesh, Neil V. Murray

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.