Trie Based Subsumption and Improving the pi-Trie Algorithm∗

An algorithm that stores the prime implicates of a propositional logical formula in a trie was de-veloped in [10]. In this paper, an improved version of that pi-trie algorithm is presented. It achieves its speedup primarily by significantly decreasing subsumption testing. Preliminary experiments indicate the new algorithm to be substantially faster and the trie based subsumption tests to be considerably more efficient than the clause by clause approach originally employed.