Application Description

This benchmark implements Survey Propagation, a heuristic SAT-solver based on Bayesian inference [1]. The algorithm represents the Boolean formula as a factor graph, which is a bipartite graph with variables on one side and clauses on the other. An edge connects a variable to a clause if the variable participates in the clause. The edge is given a value of -1 if the literal in the clause is negated, and +1 otherwise. The general strategy of Survey Propagation is to iteratively update each variable with the likelihood that it should be assigned a truth value of true or false. The data parallelism in this algorithm arises from the worklist of all the nodes (both variables and clauses) that need to be processed.

Algorithm

The algorithm proceeds as follows (pseudocode is provided in Figure 1). At each step, Survey Propagation chooses a node at random and processes it. To process a node, the algorithm updates the value of the node based on the values of its neighbors. After a number of updates, the value for a variable may become "frozen", i.e., set to true or false. At that point, the variable is removed from the graph. If a node is not frozen, it is returned to the worklist to be processed again. As the algorithm progresses and variables become frozen, the graph begins to shrink. Note that although the algorithm chooses variables to update at random, the algorithm is nonetheless highly order dependent: different orders of processing will lead to variables becoming frozen at different times.

The termination condition for Survey Propagation is fairly complex: when the number of variables is small enough, the Survey Propagation iterations are terminated, and the remaining problem is solved using a local heuristic such as WalkSAT. Alternatively, if there is no progress after some number of iterations, the algorithm may just give up.

 1:  FactorGraph f = /* read initial formula */;
 2:  wl.put(f.clausesAndVariables());
 3:  foreach Node n in wl {
 4:    if (/* time out or number of variables is small */) {
 5:      break;
 6:    }
 7:    if (n.isVariable()) {
 8:      n.updateVariable();
 9:      if (/* n is frozen */) {
 10:       /* remove n from graph */
 11:       continue;
 12:     }
 13:   } else {
 14:     n.updateClause();
 15:   }
 16:   wl.add(n);
 17: }

Data Structures

• Unordered Set

  : Because the algorithm is based on iteratively updating the values of variables chosen at random, the worklist can be represented as an unordered set. There are no ordering constraints on the processing the elements of the worklist (although, as discussed above, different orders of processing may lead to different algorithmic behavior).

• Factor Graph

  : The bipartite graph representing the Boolean formula.

Parallelism

The active nodes in Survey Propagation are the clauses and variables of the factor graph; in other words, every node in the graph is an active node, and they can be processed in any order. Because processing a node requires reading its neighbors, two nodes can be processed in parallel as long as they are not neighbors. If a variable node needs to be removed from the graph because it is frozen, this restriction becomes tighter. Because removing a variable from the factor graph requires updating the edge information at the neighboring clause nodes, an iteration that removes a variable cannot occur concurrently with an iteration that reads or writes one of the neighboring clauses.

Figures 2 and 3 show the available parallelism and the parallelism intensity of Survey Propagation, respectively, for a random input consisting of 500 variables and 2100 clauses. Each iteration of survey propagation touches a single node in the factor graph and a small neighborhood around that node. Iterations conflict with one another if those neighborhoods overlap. The structure of the graph is largely constant, except for occasionally removing a node. Thus, the available parallelism reflects the connectivity of the graph and remains roughly constant, dropping occasionally as nodes are removed from the graph. Note that survey propagation terminates before the worklist is empty. The parallelism intensity increases slightly as nodes are removed from the graph because doing so reduces the connectivity of the graph, making it less likely that two iterations will conflict.