This talk presents a tautology checking algorithm that is related both to Stalmarck's algorithm and the mechanism described by Kunz and Stoffel in "Reasoning in Boolean Networks". The algorithm uses as its central data structure the conjunction of a set of terms, with each term being a relation over a small number of variables. In Stalmarck's algorithm the relation is limited to Boolean operators with up to two operand variables and one result variable. The new algorithm generalises this to allow arbitrary relations over three boolean variables, and then further extended to allow relations over as many as eight boolean variables. These extensions greatly increase the number and power of the inference rules that may be applied. Efficient processing relies on the use of bit patterns (8- or 256-bit) to represent the relations.

Another extension is to increase the richness of the variable mapping information obtained from the inference rule applications. In Stalmarck's algorithm, the mapping information is a set of equalities/inequalities between pairs of variables. This is extended to arbitrary relations over boolean pairs.

The talk may include test results showing how these extensions effect the depth of recursion needed and the number of terms required at each level.

Keywords
Tautology checking, Boolean satisfiability, Boolean networks, digital circuit verification, MCPL.