next up previous contents
Next: Locally Skewed, Globally Balanced Up: Reference - Search heuristics Previous: Reference - Search heuristics   Contents

State Machines Used to Represent Functions (SMURFs)

Prior to searching, Boolean functions become implemented as acyclic Mealy machines, called SMURFs (for ``State Machine Used to Represent Functions''). SMURFs help lower the overhead of searching and make complex search heuristics feasible: all important data needed for the search process and able to be computed prior to search is memoized in SMURF states and transitions for immediate access during search. The inputs to a SMURF are literals that are assumed or inferred, during search, to be true; the outputs are sets of literals that are forced to be true (analogous to unit resolution in CNF) by the newly assigned inputs; and the states correspond to what ``portion'', or residual, of the constraint remains to be satisfied11. SMURFs are described in Figure [*]. For a set of constraint BDDs, we compute the SMURFs for each of the separate BDDs and merge states with equal residual functions, maintaining one pointer into the resultant automaton for the current state of each constraint.

Figure: BDDs are preprocessed into deterministic Mealy machines called ``SMURFs.'' This example explains construction. ite denotes if-then-else and $\oplus$ denotes exclusive or.

The SMURF above represents $\mbox{\sl
ite}(x_1,x_2\wedge(x_3\oplus x_4),x_4\wedge(x_2\oplus x_3))$. It represents, in part, BDDs for the function under all possible variable orderings -- since we cannot know in what order the brancher considers the variables.
The start state (upper left) represents the original function. On the left is a transition from the start state labeled ``$x_1;x_2$''; this means that, from that state, on input $x_1$, the automaton makes a transition and outputs $\{x_2\}$. If the brancher guesses, or infers, that $x_1$ is true, it will ``tell'' the automaton to branch on $x_1$. The output of $\{x_2\}$ tells the brancher that $x_2$ must also be true -- the analogue of unit inference in CNF. This transition goes to a state labeled $x_3\oplus x_4$, meaning that, after $x_1,x_2$ are set to 1, what remains to be satisfied -- the residual function -- is $x_3\oplus x_4$. On the upper right are three transitions shown with one arrow. The first is from the start state on input $\neg
x_2$; it outputs $\{\neg x_1,x_3,x_4\}$ and goes to state 1 -- meaning the original BDD is now satisfied, i.e., that there is no residual constraint to satisfy.

The SMURF structure described in the figure, for a Boolean function with $n$ variables, can have, in the worst case, close to $3^n$ states. Thus, an Achilles' heel of SBSAT can be handling long input functions. In most benchmarks, that has not been a serious practical problem because all individual constraint are reasonably short except12 for a small special group of functions: long clauses, long exclusive disjunctions, and ``assignments'' $\lambda_0=\lambda_1\wedge\cdots\wedge\lambda_k$ and $\lambda_0=\lambda_1\vee\cdots\vee\lambda_k$ (where the $\lambda_i$'s are literals). To solve the space problem for these special functions, we create special data structures; these take little space and can simulate the SMURFs for the functions exactly with little time loss. For a long clause we store only (i) whether the clause is already satisfied, and (ii) how many literals are currently not assigned truth values. Storing exclusive disjuncts is similar. For the assignments, we store both the value (0,1, or unassigned) of the left-hand-side literal and the number of right-hand-side literals with undefined truth values.

next up previous contents
Next: Locally Skewed, Globally Balanced Up: Reference - Search heuristics Previous: Reference - Search heuristics   Contents
John Franco 2011-09-15