Parallel SAT Solver

by Patrick Wang & Sihao Ren

Summary

We are going to implement different SAT solver algorithms.
We are going to parallel these programs by using CPUs via OpenMP and MPI.
We are going to compare our parallel-version SAT solver with other mature SAT solvers.

Background

The Boolean satisfiability problem (abbreviated SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. SAT is the first problem that was proven to be NP-complete.

Our work is based on ManySAT 2.0, which is the first deterministic parallel SAT solver. ManySAT 2.0 is a portfolio-based parallel SAT solver for shared memory multi-core systems. It launches multiple SAT solvers with different search strategies in parallel, and each solver tries to solve the same SAT instance competitively.

The Challenges

1. Overall Challenge

There are several challenges in this project.

First, the choice of all sorts of algorithms plays an important role in performance.

Second, the way we parallel our program, like OpenMP and MPI.

Third, the strategies we choose to parallel our program. There are mainly two approaches of parallel SAT solving: portfolio and divide-and-conquer approaches. The former approach launches multiple SAT solvers with different search strategies in parallel, and each solver tries to solve the same SAT instance competitively. The latter approach divide a given SAT instance in an attempt to distribute the total workload among computing units, and then solve them in parallel. In both approaches, clause exchange techniques are combined into parallel systems in order to share the pruning information of the search space between solvers[1]. So, there is a question that is it possible to combine these two approaches? Will the combined approach be better than these two approaches separately?

Fourth, the performance of parallel implementation may depend on different algorithms, some algorithms could have worse performance in their sequential version, but they may be able to parallel better.

Fifth, the performance of our program also depends on different satisfiability problems and data sets.

Sixth, how do we benchmark our parallelized-version program for challenges we discussed above. For a certain algorithm, we can compare our parallelized version with sequential version. However, we should also compare our parallelized program to other SAT solver, like Z3 solver, to test the overall performance of all sorts of SAT problems.

2. Detailed Challenges:

First, clause exchange is a cooperative and fundamental mechanism in parallel SAT solvers in order to share the pruning information of the search space between computing units. Each computing unit periodically receives clauses from the other computing units. Obviously, An efficient communication between computing units is the key to a good performance of a parallel SAT solver. Therefore, how to communicate with other computing units more efficiently? Is shared-memory communication model or message passing communication model more suitable in the situation? Is there any way to reduce the communication cost, like improving temporal locality, improving arthmetic intensity and reducing contention?

Second, The reception interval for the pruned information from the other computing units is called a period. Obviously, period is also an important factor that influences the parallel performance. Therefore, the challenge here is how to determine a proper value of period? To achieve a deterministic solver, the value must be independent from a particular instance or machine or a fixed value. And the value should be stable enough since a flucuated period would increase the communication cost. In ManySAT 2.0, the length of a period is defined as the number of conflicts. Is there any other strategy to set a more stable value of period?

Third, To make the parallel SAT solver deterministic to benchmark the parallel performance, a synchronization mechanism is required. Figure 1 from ManySAT 2.0 paper shows the waiting time ratio for each instance. “det-static” and “det-dynamic” denote the results of the static and dynamic periods, respectively.

Fig. 1. Waiting time ratio of ManySAT with static and dynamic periods. The ratio is defined for each instance as the total waiting time of all threads divided by the total solving time of all threads. Results are sorted by the ratio.

These results indicate that there is high waiting time ratio to the running time. So, reducing the idle time of computing units is another important factor that influences the parallel performance. Therefore, the challenge here is how to eliminate these idle time. Is there a suitable asynchronous clause exchange strategy be used to hide these idle time? Is there a dynamic assignment strategy that makes the work more even?

Resrouces

GHC Machine

Eight-core, 3.0 GHz Intel Core i7 processor (although dynamic frequency scaling can take them to 4.7 GHz)

Pittsburgh Super Computer

1. Regular Memory (512x)

CPU: 2x AMD EPYC 7742 (2.25-3.40 GHz, 2x64 cores per node)
RAM: 256 GB
Cache: 256 MB L3 cache, 8 memory channels
Local Storage: 3.84 TB NVMe SSD
Network: Mellanox ConnectX-6-HDR Infiniband 200Gb/s Adapter

2. V100 GPU (9x)

GPU: 8x NVIDIA V100-16GB
CPU: 2x Intel Xeon Gold 6148 (2.40-3.70 GHz, 2x20 cores per node)
RAM: 192 GB, DDR4-2933
Interconnect: PCIe
Cache: 2.75 MB last level cache, 6 memory channels
Local Storage: 4x 2 TB NVMe SSD
Network: 2x Mellanox ConnectX-6-HDR Infiniband 200Gb/s Adapter

Goals and Deliverables

Plan to Achieve

Implement different-version SAT algorithms with portfolio approach, a version with divide-and-conquer approach, and a version combining portfolio and divide-and-conquer approaches, and compare their performance.
Implement OpenMP and MPI versions of these algorithms, and try to reduce the communication cost in any possible strategy and compare the optimized version with the non-optimized version.
Find a strategy to set a proper period, and compare the optimized version with the non-optimized version (The same strategy with ManySAT 2.0).
Find a strategy to reduce the waiting time, and compare the optimized version with the non-optimized version (The same strategy with ManySAT 2.0).

Hope to Achieve

Our parallel SAT solver has good performance on all sorts of SAT problems.
Our parallel SAT solver could have some comparability with other SAT solvers.

Platform Choice

GHC machines
Pittsburgh Super Computer

Schedule

Week 1: Read recent research paper on different SAT algorithms.
Week 2: Implement different sequential versions of SAT algorithms.
Week 3: Implement OpenMP version of chosen SAT algorithm.
Week 4: Implement MPI version of chosen SAT algorithm.
Week 5: Reduce the waiting time and set a proper period, and compare the optimized version with the non-optimized version.
Week 6: Further Optimization of our parallel program and write report.

Reference

[1] Hamadi, Y., Jabbour, S., Piette, C. and Sais, L., 2011. Deterministic parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation, 7(4), pp.127-132.

Page updated

Google Sites

Report abuse