Parallel Conflict-Driven Clause Learning (CDCL) SAT Solver

Team Members: Alan Joseph (alanjose), Om Arora (oarora)

Course: 15-418 - Parallel Computer Architecture and Programming, Spring 2026

Project URL: https://alanj268.github.io/parallel-SAT-CDCL

Project proposal page for the 15-418 final project.

Milestone Report

Summary

We will build a high-performance parallel SAT solver by parallelizing key components of the Conflict-Driven Clause Learning (CDCL) algorithm: portfolio-style search and inter-worker learned clause sharing. The implementation targets multi-core CPUs on GHC lab machines using C++ and OpenMP, with additional scaling experiments on PSC/Bridges-2 if time permits. Our goal is to quantify how much parallel search plus selective clause exchange can improve throughput and time-to-solution over a strong sequential CDCL baseline.

Background

Application Context

SAT asks whether a propositional formula in CNF has a satisfying truth assignment. Although SAT is NP-complete in the worst case, modern CDCL solvers are central to hardware/software verification, AI planning, and combinatorial optimization because they exploit structure in real-world instances.

CDCL Core Loop

CDCL alternates between decisions, Boolean Constraint Propagation (BCP), conflict analysis, clause learning, and non-chronological backjumping. BCP dominates runtime and uses watched literals to efficiently detect unit clauses. Conflict analysis generates high-value learned clauses (typically via a 1-UIP cut) that prune future search. 

function CDCL(phi):
  propagate()           // level-0 unit propagation
  if conflict: return UNSAT
  while not all variables assigned:
    (x, v) <- decide()
    while True:
      conflict_clause <- propagate()
      if no conflict: break
      if decision_level == 0: return UNSAT
      (learned, bt_level) <- analyze(conflict_clause)   // 1-UIP
      add_clause(phi, learned)
      backjump(bt_level)
      assert(learned)
  return SAT, assignment

Why Parallelism Helps

In a portfolio solver, multiple workers run independent CDCL searches with different random seeds and heuristic tie-breaking. Since workers encounter different conflicts, they learn different clauses; sharing high-quality clauses can prune each other's search spaces and reduce overall solve time.

The Challenge

Workload Characteristics

System Constraints and Learning Goals

We aim to learn how algorithmic SAT heuristics interact with low-level parallel systems concerns (synchronization granularity, memory locality, and thread scheduling), and what design choices drive real speedup on irregular search workloads.

Resources

References

  1. Eén, N. and Sörensson, N. (2003). "An Extensible SAT Solver." SAT 2003, LNCS 2919.
  2. Audemard, G. and Simon, L. (2009). "Predicting Learnt Clauses Quality in Modern SAT Solvers." IJCAI 2009.
  3. Hamadi, Y., Jabbour, S., and Sais, L. (2009). "ManySAT: a Parallel SAT Solver." JSAT, 6(4).

Goals and Deliverables

Plan to Achieve (Core Success Criteria)

  1. Correct sequential CDCL solver with watched literals, 1-UIP analysis, VSIDS, clause deletion, and restart policy.
  2. OpenMP portfolio solver with p workers and robust SAT/UNSAT termination protocol.
  3. Thread-safe clause-sharing channel and worker-side import/export integration.
  4. Quality filtering (initially LBD threshold l, tuned experimentally).
  5. Performance evaluation at 1/2/4/8 threads on GHC, targeting roughly 4x–6x speedup on hard instances versus sequential baseline.
  6. Correctness validation: SAT solutions checked by independent verifier; UNSAT cross-checked against sequential baseline.

Hope to Achieve (Stretch)

  1. Scaling studies on PSC/Bridges-2 (16/32/64 threads).
  2. Adaptive sharing throttle based on worker conflict rate and queue pressure.
  3. Comparative study of clause filtering strategies (LBD vs. length vs. activity).
  4. Optional UNSAT certificate generation if core milestones are complete early.

Fallback Goals (If Progress Is Slower)

If full shared-clause integration becomes unstable or too costly within the timeline, we will deliver a correct no-sharing parallel portfolio solver plus a rigorous analysis of where speedup is gained and where it is lost.

Deliverables

Platform Choice

Multi-core CPUs with OpenMP are a strong fit for CDCL portfolio solving because workers can share learned clauses through low-latency shared memory rather than message serialization. This model mirrors successful industrial parallel SAT designs and allows rapid iteration on synchronization policies and memory layout. It also maps naturally from 8-core GHC hosts to higher-core-count PSC nodes for scalability analysis.

Schedule

Key Deadlines:
  • Milestone Report Due: Tuesday, April 14th, 11:59pm
  • Final Report Due: Thursday, April 30th, 11:59pm
  • Poster Session (15-418 groups): Friday, May 1st, 8:30–11:30am

Week 1 (Mar 25 – Mar 31): Sequential Core Infrastructure

Week 2 (Apr 1 – Apr 7): Complete Sequential CDCL

Week 3 (Apr 8 – Apr 14): Parallel Framework + Milestone

Week 4 (Apr 15 – Apr 21): Optimization and Profiling

Week 5 (Apr 22 – Apr 28): Full Evaluation + Poster Draft

Week 6 (Apr 29 – May 1): Finalization and Submission