Survey: Parallelizing SAT Solvers

Jiang Long
CS267 EECS@UC-Berkeley
Spring 2010

January 31, 2010

Contents

1 Brief Bio
2 Parallelizing SAT Solvers
 2.1 Background
  2.1.1 SAT Solver Primer
 2.2 Parallelizing SAT Solvers
3 Future Directions

1 Brief Bio

I am a second year PhD candidate in EECS department, working with Prof. Robert Brayton. My research interest in synergy between synthesis and verification.

I came from China with BS degree in Computer Science and got M.S. in Computer Science Univ of Texas at Austin.

From this class, I would like to learn the state-of-art parallel paradigm on various applications, especially at the MPI and PThread level. The application I am interested in is EDA algorithms which were memory/performance driven application, very specialized and optimized for capacity. Multi-cores and computer farms open door for further gain in performance, however the difficulty is to partition the original problem to take advantage the extra CPU resources now available, to devise scalable and efficient parallel version of the original algorithms, maintaining robustness and stability.

I am an experienced C/C++ programmer, have some experience programming parallel application using PThreads.

2 Parallelizing SAT Solvers

2.1 Background

Satisfiability solving has been studied for the last twenty years. Advances have been made achieving order of magnitude of improvement, allowing SAT solvers to be used on many applications including formal verification of digital designs. However, performance and capacity of SAT solving are still very limited. With the advances of multi-core, multi-cpu and computer farms, efforts have been made to parallelize SAT solving utilizing the available resources, to expedite the performance of SAT solvers.

2.1.1 SAT Solver Primer

The procedure in Figure 1 gives a generic procedure of modern SAT solves based on DPLL. The major component are the following:

  1. Choose_decision_var: choose a variable split
  2. BCP_Propagate : Boolean constraint propagation
  3. Analyze_conflict & Back_track: Conflict analysis for non-chronological backtracking

 
int  SAT_solve() {  
   while(1) {  
     var = Choose_decision_var();  
     if ( var == NULL) return SAT;  
     while ( BCP_Propagate() == CONFLICT ){  
       Analyze_conflict();  
       Back_track();_  
       if(decision_level<0) return UNSAT;  
     }  
  }  
}  


Figure 1: Generic SAT solver procedure

The following are the key aspects that effects SAT solver performance:

  1. Static learning to obtain smaller CNF formula
  2. BCP_Propagate take 70% to 90% of an actual SAT run, for which cache locality is essential.
  3. Learning smaller conflict clauses can shorten the search space exponentially.

2.2 Parallelizing SAT Solvers

Recent effort on parallelizing SAT solvers has not been successful. During a SAT run, SAT solver generates learned clauses to prune future search space. With multiple instance of SAT solvers running at the same time, it is desirable to share clauses between solvers. This has been the focus of recent parallel solvers. However, it is rather difficult to share clauses because of the following:

  1. Communication cost: the size of generated clauses can be rather huge for a short period of running
  2. Which clauses to share: it is rather hard to pick which subset of learned conflict clauses to be shared across solver instances, because it can incur considerable performance degradation if the added clauses are of no use. Moreover, it is computation intensive to check for duplicate and redundant clauses.
  3. When to synchronize: the correctness of Solver needs to be maintained, thus the synchronization point of sharing/communicating needs be designed carefully.
  4. Cache performance: For shared memory implementations, the added cost of synchronization and overhead will degrade the cache performance which is highly important to SAT solving.
  5. Partitioning: Because of the size of the SAT problem and its consistency requirement, it is very hard to partition the problem to apply divide-and-conquer framework, because any partition is likely an under-approximation of the original problem.

For the above reasons, parallelizing SAT solvers has not been successful at all.

3 Future Directions

To achieve effective parallelization of SAT solvers the following are considered key given current research results:

  1. High-level learning rather than learning at the clause level.
  2. Effective partitioning of the original SAT problem such that learning from different partitions can be utilized in other partitions.
  3. Implementing various solver and learning instances such that the complexity of the original problem is reduced in combination.