Aitong (Ivy) Li • Ananya Aggarwal
https://aitongl.github.io/
We will build a parallel Maximum Satisfiability (MaxSAT) solver by starting from a sequential CDCL SAT solver and implementing a core-guided MaxSAT algorithm on top of it. Our system will expose solver internals such as learned clauses and conflicts, and then introduce parallelism at the MaxSAT level by coordinating multiple workers.
Workers will explore different parts of the search while selectively sharing useful information such as unsatisfiable cores, bounds, and high-quality learned clauses to reduce redundant computation.
Maximum Satisfiability (MaxSAT) extends SAT by allowing some clauses to be “soft” and seeking an assignment that maximizes the number of satisfied clauses.
Maximum satisfiability is an NP-complete problem, meaning solving it efficiently could help solve many real-world problems such as the traveling salesman problem.
We aim to design a parallel MaxSAT solver using communication protocols such as OpenMP and experiment with different communication strategies.
The main bottleneck is repeated SAT solving, which makes this problem well-suited for parallelism, though coordination between workers is required.
MaxSAT has strong dependencies across iterations. Each SAT call depends on previously learned cores, making naive parallelization ineffective.
Another challenge is deciding what information to share. Sharing too much increases overhead, while sharing too little reduces the benefits of parallelism.
The workload involves irregular control flow, communication overhead, and potential load imbalance between workers.
We will use the open-source Glucose SAT solver as a base and modify it to expose internals such as learned clauses and conflicts.
We will also use industry-standard benchmarks and PSC cluster resources for evaluation.
A correct sequential solver and a basic parallel version with limited communication and evaluation.
We aim to understand how much of MaxSAT can be parallelized, what information sharing is most effective, and how communication impacts performance.
We will also study how solver internals influence parallel efficiency.
The system will support coordinated parallel solving with configurable communication strategies.
We expect improved performance over sequential solvers on larger instances, though not linear scaling due to dependencies.
We will use C++ with the Glucose solver and OpenMP/thread-based parallelism on PSC systems.