← Back to Proposal

Milestone Report

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

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

Milestone Report – April 14, 2026

Work Done So Far

We are a little behind on planned schedule. So far, we have a working version of the CDCL SAT solver. We implemented it from scratch, using the Extensible SAT solver paper[1]. The solver supports input SAT instances in DIMACS format, and uses the two-literal watching data structure with BCP. It then uses 1-UIP conflict analysis to produce learnt clauses, and adds it to a list of learnt clauses that are used to avoid future conflicts. A few optimizations remain to be performed, namely, using VSIDS variable heap activity when deciding which literal to assign next, implementing some form of clause deletion to evict low-quality learnt clauses, and Luby restart sequence policy to escape from certain branches of the solution space.

[1] Eén, N. and Sörensson, N. (2003). "An Extensible SAT Solver." SAT 2003, LNCS 2919.

Goals and Deliverables

We still plan to hit all our "Plan to Achieve" goals by the project deadline, even though we are a little behind. We will deliver a correct, working, parallel portfolio based CDCL SAT solver with clause sharing data structures using OpenMP, optimized for performance on the GHC machines. From our "Hope to Achieve" goals, we hope to test and optimize for scalability on the PSC Bridges-2 cluster. If time permits, we can also empirically analyze further clause sharing strategies (such as LBD-based filtering vs. clause length vs. activity-based filtering). It seems we will not be able to attempt the adaptive clause sharing throttle and clause freezing strategies we proposed originally, and we will likely not focus on generating UNSAT certificates.

Goals for the Poster Session

Note: "Hope to Achieve" goals are marked with an asterisk (*).

  1. Correct Sequential CDCL baseline (already completed)
  2. Multi-threaded portfolio solver (15th – 18th April, Om)
  3. Basic clause sharing protocol (19th – 22nd April, Alan)
  4. Quality filter (23rd – 25th April, Om)
  5. Correctness validation & performance evaluation (26th – 30th April, Alan)
  6. (*) Performance evaluation and optimization on PSC Bridges-2
  7. (*) Empirically analyze different clause sharing strategies

Demo Plan

We plan to show speedup graphs comparing our parallel SAT solver with our sequential one and comparing their performances on the GHC machines and the PSC machines (if time permits). We will also have graphs that show the sensitivity of the speedups on various factors of the solver, such as clause deletion rate, l, etc. We can also present an interactive demo of SAT solvers with some instances of problems.

Remaining Issues

Since we are behind schedule, we are concerned about the timeline. We need to implement a few of the optimizations for the sequential solver (namely, the VSIDS variable heap activity, clause deletion, and restarts), and then build the parallel solver. Moreover, the clause sharing requires making a multi-producer multi-consumer queue for sharing the learned clauses with all other threads.

However, over the course of building the SAT solver, we have overcome a steep learning curve and gained better intuition about its internal workings, so we believe that the optimizations and parallelization will be much faster. As such, we think we can deliver all the adjusted goals listed above.