Survey Propagation

Problem 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.

[1] A. Braunstein, M. Mezard, and R. Zecchina. Survey Propagation: An Algorithm for Satisfiability. Random Structures and Algorithms, 27:201-226, 2005.

Algorithm

The algorithm proceeds as follows. Each phase of the algorithm first iterates over the variables and clauses of the formula updating 'surveys' until all updates are below some small epsilon. Then, the surveys are processed to find the most biased variables which are fixed to a specific value. The graph is then reduced by removing fixed variables. If only trivial surveys exist, the problem is passed on to a simpler solver. If remaining terms exist, a new phase is started.

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.

The benchmark performs as many phases of the algorithm as necessary until no more variables can be fixed.

FactorGraph f = generateRandomFormula(); 
do { 
  foreach variable v { 
    foreach clause c: f.getNeighbors(v)) { 
      update_eta_and_bias(v, c); 
      if eta[c] changed more than epsilon { 
        anotheriteration = true; 
      } 
    } 
  }
  foreach variable v { 
    if bias[v] > threshold-bias { 
      fix v; 
      remove v from graph; 
    } 
  } 
} while anotheriteration;
The body of the two outer for-loops are implemented as two kernels. The kernels are repeatedly called from the host until there are no more surveys to be propagated.

Performance

The benchmark is written in CUDA.
Compile as: make
Execute as: sp <seed> <nclauses> <nliterals> <literals-per-clause>
e.g., sp 0 4200000 1000000 3

File (M-N-K)Time (ms)
random-16800-4000-3.cnf755.651
random-42000-10000-3.cnf1725.46
random-42000-10000-5.cnf63.19

The above performance is observed on a 1.45 GHz Quadro 6000 with 6 GB of main memory and 448 cores distributed over 14 SMs. It has 64 kB of fast memory per SM that is split between the L1 data cache and the shared memory.