Next: Branch Pruning Up: Reference - Preprocessing Previous: Pattern Matching: CNF   Contents

## Generalized Cofactor (GCF)

The generalized cofactor operation, denoted by gcf here and also known as constrain in the literature, uses sibling substitution to reduce BDD size. However, unlike Prune, it can produce BDDs far larger than the original. Given two functions, and , the function is such that is the same as . In the process, may be somehow reduced compared to as is the case for Prune. Unlike Prune, the following is true as well:

This means that, for the purposes of a solver, generalized cofactoring can be used to eliminate one of the BDDs among a given conjoined set of BDDs: the solver finds an assignment satisfying and then extends the assignment to satisfy , otherwise the solver reports that the instance has no solution. However, unlike Prune, generalized cofactoring cannot by itself reduce the number of variables in a given collection of BDDs. Other properties of the gcf operation are:

1. gcf gcf.
2. gcfgcf gcf .
3. gcf gcf gcf.
4. gcf gcf.
5. gcf gcf gcf.
6. gcf gcf gcf.
7. gcf gcf.
8. gcf gcf.
9. If and have no variables in common and is satisfiable then .

Care must be taken when cofactoring in both'' directions (exchanging for ). For example, cannot be replaced by since the former may be unsatisfiable when the latter is satisfiable.

The pseudo C++ description of gcf is as follows:

BDD gcf (BDD f, BDD c) {
if (f == F || c == F) return F;
if (c == T || f == T) return f;
let ;
// is the top variable of f and c
if (Reduce(, c) == F) return gcf(Reduce(, f), Reduce(, c));
if (Reduce(, c) == F) return gcf(Reduce(, f), Reduce(, c));
let = gcf(Reduce(, f), Reduce(, c));
let = gcf(Reduce(, f), Reduce(, c));
if ( == ) return ;