A new algorithm for computing theory prime implicates compilations
Pierre Marquis, Samira Sadaoui · National Conference on Artificial Intelligence · 1996
We present a new algorithm (called TPI/BDD) for computing the theory prime implicates compilation of a knowledge base Σ. In contrast to many compilation algorithms, TPI/BDD does not require the prime implicates of Σ to be generated. Since their number can easily be exponential in the size of Σ, TPI/BDD can save a lot of computing. Thanks to TPI/BDD, we can now conceive of compiling knowledge bases impossible to before.