next up previous contents
Next: Clustering + Existential Quantification Up: Reference - Preprocessing Previous: Inferences   Contents


Existential quantification

A Boolean function which can be written

\begin{displaymath}f(x, {\vec g}) = (x\wedge h_1({\vec g})) \vee (\neg x\wedge h_2({\vec g}))\end{displaymath}

can be replaced by

\begin{displaymath}f({\vec g}) = h_1({\vec g}) \vee h_2({\vec g})\end{displaymath}

where ${\vec g}$ is a list of one or more variables. There is a solution to $f({\vec g})$ if and only if there is a solution to $f(x,{\vec g})$ so it is sufficient to solve $f({\vec g})$ to get a solution to $f(x,{\vec g})$. Obtaining $f({\vec g})$ from $f(x,{\vec g})$ is known as existentially quantifying $x$ away from $f(x,{\vec g})$. This operation is efficiently handled if $f(x,{\vec g})$ is represented by a BDD. However, since problems handled by SBSAT include conjunctions of functions and therefore ``conjunctions'' of BDDs, existentially quantifying away a variable x succeeds easily only when only one of the ``conjoined'' BDDs contains x. Thus, this operation is typically used in conjunction with other preprocessing options for maximum effectiveness.

Figure: Two examples of existentially quantifying away a variable from a function. Functions are represented as BDDs on the left. Variable $x_3$ is existentially quantified away from the top BDD leaving T, meaning that regardless of assignments given to variables $x_1$ and $x_2$ there is always an assignment to $x_3$ which satisfies the function. Variable $x_2$ is existentially quantified away from the bottom BDD leaving the inference $x_1 = T$.
\begin{figure}\centerline{\epsfig{figure=Fig/exquant_bdd.eps, width=3.5in}}\end{figure}

The following is a pseudo C++ implementation ($\vee$ denotes the ``or'' of two BDDs):


BDD ExQuant (BDD f, variable x) {
if (root(f) == x) return true(root(f))$\vee$false(root(f));
if (index(x) > index(root(f))) return f; // If x is not in f do nothing
let $h_{f_T}$ = ExQuant(true(root(f)), x);
let $h_{f_F}$ = ExQuant(false(root(f)), x);
if ($h_{f_F}$ == $h_{f_T}$) return $h_{f_T}$;
return find_or_add_node (root(f), $h_{f_T}$, $h_{f_F}$);
}


Although this operation itself can uncover inferences (see, for example, Figure [*]), those same inferences are revealed during BDD construction due to the particular way we build BDDs which includes developing inference lists for each node (see Section [*]). Inferences that would be caught later by existential quantification exist in the BDD root node inference lists and may be applied early. Therefore, existential quantification is used by sbsat primarily to assist other operations, such as strengthening (see Section [*]), to uncover those inferences that cannot be found during BDD construction. Examples of the use of this operation are shown in Figure [*].

Existential quantification tends to speed up searching (that is, it results in more choicepoints per second) but tends to increase the number of choicepoints. The reason for the latter is that the elimination of a variable may cause subfunctions that had been linked only by that variable to become merged with the result that the distinction between the subfunctions becomes blurred. This is illustrated in Figure [*].

Figure: Existential quantification can cause blurring of functional relationships. The top function is seen to separate variables $x_1$, $x_2$, and $x_3$ from $x_4$, $x_5$, and $x_6$ if $x_7$ is chosen during search first. Existentially quantifying $x_7$ away from the top function before search results in the bottom function in which no such separation is immediately evident. Without existential quantification the assignment $x_8=F$, $x_7=T$, $x_6=T$ reveals the inference $x_5=T$. With existential quantification the assignment must be augmented with $x_2=F$ and $x_1=F$ (but $x_7$ is no longer necessary) to get the same inference.
\begin{figure}\centerline{\epsfig{figure=Fig/exquantex.eps, width=3.5in}}
\vspace*{10mm}
\centerline{\epsfig{figure=Fig/exquantex1.eps, width=3.5in}}
\end{figure}

On the other hand there are fewer inferences to be made during search (``or''ing two functions removes all the F terminals that can be) so the time per choicepoint decreases. The speedup can overcome the lost intelligence but it is sometimes better to turn it off. The major benefit of existential quantification is the smaller search space.

If existential quantification is selected to occur during preprocessing (named in the command-line preprocessing sequence), when invoked, for every variable, the number of BDDs in which that variable is included is determined. If the number is one, existential quantification is applied to that variable in that BDD and the process continues until no variables are included in a single BDD. Thus, after existential quantification, all variables are in at least two BDDs.


next up previous contents
Next: Clustering + Existential Quantification Up: Reference - Preprocessing Previous: Inferences   Contents
John Franco 2011-09-15