On Anti-Links

The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. The operations have linear time complexity in the size of that part of the formula containing the anti-link. These operations are useful for prime implicant/implicate algorithms because most of the computational effort in such algorithms is spent on subsumption checks.

• Type: Conference
• Year: 1994
• Where: LPAR
• Authors: Bernard Becker, Reiner Hähnle, Anavai Ramesh, Neil V. Murray
• Keywords: Automated Reasoning, LPAR 1994, Normal Form Formula, Prime Implicant/implicate Algorithms, Useful Equivalence-preserving Operations