DNF Minimizer

This Prolog program provides the core functionality for Mode 3 in the C# Boolean Utilities program Yabeu. It takes a set of disjunctive normal form clauses and reduces them to their simplest form using the Quine-McClusky algorithm. The following discussion is intended to help you find your way around the code and relate it to the stages of the minimization algorithm. Note that the Prolog source code is available as part of the YABEU source package.

Overview

The program defines a module, which provides the following exports:

        :- module(dnf_reduce, [minimize_clauseset/2,
                               op(900, fx, ~)
        ]).

The predicate minimize_clauseset/2 does all the hard work. The operator definition is required for the input and output to this predicate. The first argument to minimize_clauseset/2 must be instantiated to a list of disjunctive nromal form clauses, where each clause is a list of literals, with negative literals being indicated with the shown prefix operator. For example, the following input has three clauses, each with three literals:

[[a, b, ~c], [a, ~b, c], [a, b, c]]

The second argument must be a variable, which will be instantiated with the minimized clause set on successful execution. The following example shows this:

?- minimize_clauseset([[a, b, ~c], [a, ~b, c], [a, b, c]], M).
M = [[a, b], [a, c]].

Quine-McClusky

As noted above, the program uses the Quine-McClusky algorithm. A good discussion of this, including an example Java program that performs the same function, can be found here. The following discussion analyses each stage of the Prolog program and relates it to the algorithm. Note that the implementation makes extensive use of ordered sets.

Prime Implicants

Once the clauses have been indexed, the first step is to determine the prime implicants of the clause set. This is implemented by the module internal predicate prime_implicants/2.

To understand what a prime implicant is, consider the following example of an inference in Boolean algebra:

If we have the expression: (a & b & c) | (a & b & ~c), then we can simplify this to (a & b). In Prolog list notation, this would be expressed as:

From [[a, b, c], [a, b, ~c]] we can generate [[a, b]].

More generally, if two clauses are identical except for one containing a literal that is the complement of a literal in the other, then a new clause can be formed without the complemented literals. The new clause is an implicant of the first two. Following from this, a prime implicant is an implicant clause than cannot be further reduced.

Essential Prime Implicants

If a clause from the original input set gives rise to a prime implicant, then that clause is said to be covered by the prime implicant.

If a clause in the original set is covered by only one prime implicant then that prime implicant is essential and must be included in the final set. Conversely, if a clause in the original set gives rise to no prime implicants, then that original clause is also essential and must be included in the final set. This is implemented by the module internal predicate essential_implicants/3.

Any clauses in the original set that are not covered by any of the clauses in the set described in the previous paragraph are called the Remainder in this implementation. If there are no clauses in the Remainder, then the computation is complete and the set of essential prime implicates is the minimized clause set.

If there are clauses in the Remainder, then additional computation needs to be performed.

Covering the Remainder

For every clause in the remainder, a prime implicant needs to found that covers it. Further, the set of prime implicants that covers the Remainder needs to be as small as possible for the result to be a minimal set.

The Quine-McClusky algorithm does not specify exactly how this final stage of the computation is to be performed. To fill that gap, additional algorithms, such as Petrick's Method. However, because Prolog excels at search, I have simply implemented this final stage as a search algorithm in the predicate cover_missing_minterms/3. In the current version of the program it is simply a brute force search for the smallest set. For all of the examples that I have tried, this has been perfectly adequate. However, at some point I will probably implement a best-first search algorithm for comparison.

References

You might like to check out the following additional pages for more information: