Technical Reports

The ICICS/CS Reading Room


UBC CS TR-92-12 Summary

A Correct Optimized Algorithm for Incrementally Generating Prime Implicates, November 1992 Alex Kean and George Tsiknis, 15 pages

In response to the demands of some applications, we had developed an algorithm, called IPIA, to incrementally generate the prime implicates/implicants of a set of clauses. In an attempt to improve IPIA some optimizations were also presented. It was pointed out to us that some of these optimizations, namely the {\em subsumption} and {\em history restriction}, are self conflicting. Subsumption is a necessary operation to guarantee the primeness of implicates/implicants and {\em history restriction} is a scheme that exploits the history of consensus operation to avoid generating non prime implicant/implicates. The original IPIA, where {\em history restriction} was not consider, was proven correct. However, when {\em history restriction} was introduced later in the optimized version, it interacted with the subsumption operation to produce an incomplete set of prime implicants/implicates. This paper explains the problem in more details, proposes a solution and provides a proof of its correctness.


If you have any questions or comments regarding this page please send mail to help@cs.ubc.ca.