SURVEY PROPOGATION - Region3

From "Lonestar: A Suite of Parallel Irregular Programs", [http://iss.ices.utexas.edu/Publications/Papers/ispass2009.pdf]: Survey Propagation is a heuristic SAT-solver based on Bayesian inference. The algorithm represents the Boolean formula as a factor graph, 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 SP is to iteratively update each variable with the likelihood that it should be assigned a truth value of true or false. The worklist for Survey Propagation consists of all nodes (both variables and clauses) in the graph. 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.
There are two key data structures in Survey Propagation: 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.

Code Snippet

unsigned int: NLITERALS = 300000, gAvgBiasNum (array)
float: lbias (array), gMaxBias (array), gAvgBiasSum (array)
bool: lvalue (array), lsolved (array)

do{   
   if (hchanged > 0) 
   {


float limit = 0.0;
for (unsigned start=0; start<NLITERALS ; start++)
{
   if (start == 0)
   {
      if (*gAvgBiasNum > 0) 
      {
         float avgB = *gAvgBiasSum / *gAvgBiasNum;
         limit = *gMaxBias - 0.75 * avgB;
      } 
      else 
      {
         limit = *gMaxBias;
      }
   } 
   else
   {
      limit=0.0;
   }
        
   if (lsolved[start] == false && lbias[start] >= limit) 
   {
      lsolved[start] = true;
      lvalue[start] = true;
   }
}
   }
 
   ++outeriteration; 
} while (hchanged > 0 && outeriteration < MAXITERATION); // executes 3 times.