The concept of "anti-link" is defined, and useful
equivalence-preserving operations based on anti-links are
introduced.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. The operations have linear time complexity in
the size of that part of the formula containing the anti-link.
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 there exists a pair of subsumed paths
associated with an arbitrary anti-link is shown to be NP-complete.
Additional techniques based on "strictly pure full blocks" are
introduced and are also shown to eliminate redundant subsumption
checks. The effectiveness of these techniques is examined with
respect to some benchmark examples from the literature.