January 31, 2010

1 Brief Bio

2 Parallelizing SAT Solvers

2.1 Background

2.1.1 SAT Solver Primer

2.2 Parallelizing SAT Solvers

3 Future Directions

2 Parallelizing SAT Solvers

2.1 Background

2.1.1 SAT Solver Primer

2.2 Parallelizing SAT Solvers

3 Future Directions

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.

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.

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

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

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

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

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:

- Communication cost: the size of generated clauses can be rather huge for a short period of running
- 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.
- When to synchronize: the correctness of Solver needs to be maintained, thus the synchronization point of sharing/communicating needs be designed carefully.
- 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.
- 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.

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

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