Craig Holman was awarded his doctorate in Computer Science from Northwestern University at Evanston, Illinois in 1990. His dissertation was entitled Elements of an Expert System for Determining the Satisfiability of General Boolean Expressions and was supervised by Dr. Lawrence Henschen.

Several white papers have been adapted from this dissertation and are, or soon will be, available for reading :

     HTML      Boolean Expressions - An Overview

     HTML      The Random Generation of General Boolean Expressions

     HTML      The Constraint Calculus

     HTML      The Reduction of Constraint Trees

     HTML      Elegant Normal Form

     HTML      Resequencing Constraint Trees

     HTML      Boolean Expression Metrics

Some of the highlights of this dissertation are :

The Constraint Calculus, an algorithm for determining all of the models of a general Boolean expression, is presented and proven to be both sound and complete.

Algorithms for determining the satisfiability and falsifiability of general Boolean expressions are derived from the Constraint Calculus.

A method for randomly generating general Boolean expressions is introduced. This method depends upon the ability to randomly generate each n-node unlabelled tree with the same probability.

Elegant Normal Form (ENF), a canonical normal form for general Boolean expressions, is defined.

A set of eight graph transformations for reducing a general Boolean expression to ENF is presented and proven to be a complete set of reductions. Since a complete set of reductions is guaranteed to reduce a structure to a single form regardless of the order in which the reductions are applied, as long as they are exhaustively applied, algorithms for reducing expressions to ENF can be designed for efficiency without regard for optimizing the resulting structure.

An algorithm for reducing expressions to ENF is presented.

Several metrics of general Boolean expressions and their various representations under the Constraint Calculus are defined.

The results of applying the satisfiability-determination algorithm, as defined and as enhanced by the reduction-to-elegance algorithm, to 300,000 randomly generated general Boolean expressions having from 100 to 500 literals each are presented.

Preliminary identification of metrics which are good predictors of an expression's logical class (contradiction, satisfiable and falsifiable, tautology), cost of satisfiability determination, cost of reduction to elegance, and the number of literals in the resulting expression are presented.

99% of the expressions required fewer than 10,000 set operations for reduction to elegance and retained fewer than 2% of their original literals.

None of the elegant equivalents of these expressions retained more than 9% of the literals in the original expression.

100% of the contradictions were discovered to be contradictions during their reduction to elegance.

99.99% of the tautologies were discovered to be tautologies during their reduction to elegance.

84% of the expressions did not require backtracking during the final stage of the satisfiability-determination algorithm

99% of the elegant expressions did not require backtracking during the final stage of the satisfiability-determination algorithm.