next up previous contents
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, $f$ and $c$, the function $g={\tt gcf}(f,c)$ is such that $f\wedge c$ is the same as $g\wedge c$. In the process, $g$ may be somehow reduced compared to $f$ as is the case for Prune. Unlike Prune, the following is true as well:

$\textstyle \parbox{4.5in}{ Given Boolean functions $f_1,...,f_k$, for
any $1\le...
...nt satisfying the latter can be
extended to satisfy $f_1\wedge ...\wedge f_k$.}$

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 ${\tt gcf}(f_1,f_i)\wedge ...\wedge {\tt gcf}(f_k,f_i)$ and then extends the assignment to satisfy $f_i$, 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. $f=c\wedge$gcf $(f,c)\vee \neg c\wedge$gcf$(f,\neg c)$.
  2. gcf$($gcf$(f,g),c) =$ gcf $(f, g\wedge c)$.
  3. gcf $(f\wedge g, c)=$ gcf$(f,c)\wedge$ gcf$(g,c)$.
  4. gcf $(f\wedge c, c)=$ gcf$(f,c)$.
  5. gcf $(f\wedge g, c)=$ gcf$(f,c)\wedge$ gcf$(g,c)$.
  6. gcf$(f\vee g, c)=$ gcf$(f,c)\vee$ gcf$(g,c)$.
  7. gcf $(f\vee \neg c, c)=$ gcf$(f,c)$.
  8. gcf $(\neg f,c)= \neg$ gcf$(f,c)$.
  9. If $c$ and $f$ have no variables in common and $c$ is satisfiable then ${\tt gcf}(f,c) = f$.

Care must be taken when cofactoring in ``both'' directions (exchanging $f$ for $c$). For example, $f\wedge g\wedge h$ cannot be replaced by ${\tt gcf}(g,f)\wedge {\tt gcf}(f,g)\wedge h$ 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 $x_m = index^{-1}(\min\{index(root(c)), index(root(f))\})$;
// $x_m$ is the top variable of f and c
if (Reduce$_F$($x_m$, c) == F) return gcf(Reduce$_T$($x_m$, f), Reduce$_T$($x_m$, c));
if (Reduce$_T$($x_m$, c) == F) return gcf(Reduce$_F$($x_c$, f), Reduce$_F$($x_c$, c));
let $h_T$ = gcf(Reduce$_T$($x_m$, f), Reduce$_T$($x_m$, c));
let $h_F$ = gcf(Reduce$_F$($x_m$, f), Reduce$_F$($x_m$, c));
if ($h_T$ == $h_F$) return $h_T$;
return find_or_add_node($x_m$, $h_T$, $h_F$);
}

Figure: Generalized cofactor operation on $f$ and $c$ as shown. In this case the result is more complicated than $f$. The variable ordering is $x_1$, $x_2$, $x_3$, $x_4$.
\begin{figure}\hspace*{1mm}\epsfig{figure=Fig/cofactoring2a.eps, width=2.25in}
\...
...
\hspace*{30mm}\epsfig{figure=Fig/cofactoring3a.eps, width=2.5in}\end{figure}

Figure [*] presents an example of its use illustrating the possibility of increasing BDD size. Figure [*] presents the same example after swapping $x_1$ and $x_4$ under the same variable ordering and shows that result produced by gcf is sensitive to variable ordering. Observe that the functions produced by gcf in both Figures have different values under the assignment $x_1 = T$, $x_3 = T$, and $x_4 =
F$. Thus, the function returned by gcf depends on the variable ordering as well.

Figure: Generalized cofactor operation on the same $f$ and $c$ of Figure [*] and with the same variable ordering but with $x_1$ and $x_4$ swapped. In this case the result is less complicated than $f$.
\begin{figure}\hspace*{1mm}\epsfig{figure=Fig/gcf2.eps, width=3.5in}
\vspace*{-4...
...{10mm}\\
\hspace*{30mm}\epsfig{figure=Fig/gcf3.eps, width=2.25in}\end{figure}


next up previous contents
Next: Branch Pruning Up: Reference - Preprocessing Previous: Pattern Matching: CNF   Contents
John Franco 2011-09-15