Parallel Maximum Satisfiability Solver

Goals and Deliverables

Core Goals

• ✅ Understand Glucose code base.
• ✅ Implement a baseline sequential implementation of MaxSAT using the Glucose SAT solver. Test it on the industry standard benchmarks.
• ✅ Implement a baseline parallel MaxSAT solver by running multiple SAT solver instances in parallel on different parts of the search space.
• ☐ Design a more sophisticated parallel algorithm that shares clauses and other internal information using OpenMP.
• ☐ Evaluate performance on standard benchmark instances (e.g., SATLIB / MaxSAT benchmarks) using PSC cluster resources.
• ☐ Measure:
  • Speedup vs. sequential baseline
  • Scalability across cores/processors

Extended Goals

• ☐ Compare multiple communication strategies, such as:
  • No communication (independent workers)
  • Periodic clause sharing
  • Adaptive or selective clause sharing
• ☐ Implement simple load balancing or work-stealing to improve utilization.
• ☐ Explore heuristics for deciding what information to share (e.g., only high-quality learned clauses).

Half-Week Breakdown

Apr 13–16 (Responsible: Ivy)

• Understand why the current baseline parallel MaxSAT is performing worse on multiple cores. This will give us an understanding of how to implement the sophisticated algorithm.
• Select a better set of benchmarks to ensure that the test cases have room for parallelism. Rerun some testing for the previous approaches.

Apr 17–19 (Responsible: Ananya)

• Use the insights from the above analysis to implement a sophisticated parallel algorithm that takes advantage of sharing clauses and internal information.
• Brainstorm for alternative approaches to parallelism at the same time in case that clause sharing does not provide a significant advantage/speedup. If it comes up that speedup is hard in the case we want a perfect solution, try sacrificing correctness for better speedup (might not find the most optimal solution).

Apr 20–23 (Responsible: Ivy)

• Iterate on the above algorithm to maximise performance.
• Potentially explore extended goals such as exploring heuristics on what to share and maybe only sharing the high quality learned clauses.

Apr 24–26 (Responsible: Ivy)

• Record speedups and data on GHC and PSC machines. Use selected subset of standard benchmarks.
• Measure:
  • Speedup vs. sequential baseline
  • Scalability across cores/processors
  • Accuracy, if that is sacrificed in the algorithm

Apr 27–30

• Write up the prose of the report. (Responsible: Ananya)
• Generate plots and tables for report. (Responsible: Ivy)
• Clean up code for submission and ease of understanding.

Work Completed So Far

We started off by understanding how the Glucose library works. We first identified the relevant sections of the library for us and then worked on using it to implement a purely sequential MaxSAT solver. It iterates B = 0, 1, 2, ... and for each B, encode the constraint that sum(relax_vars) ≤ B and calls Glucose's solver with this assumption. Learned clauses are reused across iterations, giving the sequential solver a significant advantage over solving from scratch each time.

In addition, we also experimented with a naive parallel version that splits up the search space by partitioning the minimum number of soft clause violations. After some calibrations and testing, we decided to instead use a dynamic work queue approach that assigns the next unclaimed bound B to whichever thread finishes first, avoiding the load imbalance of static partitioning. Threads share only the current best cost atomically, allowing early termination when another thread finds a better solution.

How We're Doing with Respect to Proposal

We are doing well with respect to the core goals proposed in our project proposal. We have the first iteration of our algorithm working. However, it is not performing well across multiple cores which is a cause for concern for us. Thus we suspect this will slow down our future progress, possibly hindering our ability to expand to multiple communication protocols and other extended goals.

We still believe we will be able to achieve all our core goals as outlined in our half week breakdown.

Preliminary Results

Sequential Baseline

Parallel Version — Solve Time by Thread Count (s)

These are some of the times that were collected for the current two approaches that we implemented. We hope to come up with more appropriate benchmarks that give away for more parallelism and reevaluate the two approaches with respect to those tests.

Goals for Poster Session

• Deliver a working parallel MaxSAT solver that shares learned clauses across cores, targeting at least 2-4x speedup over the sequential baseline on hard benchmark instances.
• Collect and present performance data across 1, 2, 4, and 8 threads in GHC and possibly more threads on a set of hard benchmarks, measuring speedup, scalability, and solution quality.
• If clause sharing alone does not yield meaningful speedup, demonstrate and explain an alternative parallelism strategy (e.g., sacrificing optimality for throughput) with data justifying the tradeoff.
• Present clear graphs and a visual walkthrough of each approach — sequential baseline, naive parallel, clause-sharing parallel, or any other algorithms — highlighting advantages and disadvantages of each.

Display

We hope to provide graphs for speedups with respect to different threads during the final poster session. Currently, we have been timing our code similar to how it has been done in the previous assignments for a select few test cases.

Concerns

• The benchmark test suite is too large in terms of memory. We need to randomly select a subset.
• We used a subset of benchmark test cases to produce the milestone report, but there is a lot of variation in terms of how long each test takes. We might need to be more careful about what to pick. There are some tests that even with a simple sequential approach outputs the correct results in 0.001s. We need to instead focus on harder instances where individual SAT calls are expensive and the optimal cost is large enough that multiple B values need to be explored.
• The parallel version currently shows no speedup on the instances we tested. The main bottleneck is that each thread builds its own independent solver and counter table from scratch.
• We are also unsure if more clause sharing across cores will provide a significantly better parallel algorithm in terms of speedup.