Pranav Tatavarti & Michael Liang
URL: https://www.andrew.cmu.edu/user/mliang4/
Summary:
We plan to implement and parallelize a CDCL SAT Solver program. We plan to C++ OpenMP to achieve this. We will compare the performance of the two parallel systems to see which achieves greater speedup.
Background:
SAT solvers aim to determine the satisfiability of a Boolean circuit, i.e., whether there is a possible assignment of input variables that causes the output to evaluate to true. The modern algorithm used by SAT solvers is called CDCL (Conflict-Driven Clause Learning). The general idea is that a random variable assignment is guessed. The implications of it are calculated. If a logical contradiction occurs, the algorithm learns a new clause and backtracks. This process is repeated until all assignments are tested or a satisfiable assignment is found. There are multiple ways that parallelism can be injected into the problem. The random assignment mentioned earlier can operate based on several possible heuristics that could each get lucky or unlucky in finding a satisfiable set of inputs quickly depending on the nature of the circuit. A possible mode of parallelism is to run the same SAT solver multiple times in parallel, each with a different random assignment heuristic. This increases the odds that some heuristic gets lucky and the solution is found quicker. Another method of parallelizing the algorithm is to split the assignment space across the threads. For example, one thread could evaluate the possibilities where an input variable x is 0, and another could examine what happens when x = 1. Parallelism can further be optimized with clause sharing, where if one thread discovers that a certain section of the input variable assignment space is
The Challenge:
Professor Marjin Huele said this is
notoriously hard to parallelize. This is challenging because there are many dependencies due to the inherently sequential nature of the algorithm. For example, each step of the unit propagation process depends on the previous step. Different decisions about what to assign a variable can greatly change the resulting search space which can cause load imbalances. Certain variable assignments could also force other variables to be a certain value. One thread could try to assign a variable that exists in clauses other threads on working which would require communication. When a conflict arises the algorithm has to backtrack through the implication tree to discover the assignments that caused that conflict and this implication tree has to be consistent amongst all the processors which seems like it would require a lot of synchronization. We would also want threads to share their learned clauses with each other. There could be unpredictable dependencies between variables that are not close together in memory leading to poor locality. Additionally, parallelism doesn’t naively emerge from the structure of the algorithm. There are multiple non-obvious ways to parallelize as we discussed earlier, each bringing strengths and weaknesses. This brings about greater opportunities for optimization and testing.
Resources:
We will make the algorithm from scratch. We will use these lecture slides as a resource: https://www.cs.cmu.edu/~mheule/15311-s26/slides/CDCL.pdf. We’re going to use GHC and PSC.
Goals and Deliverables:
Plan to Achieve: Successfully implement the algorithm sequentially. Get a working implementation that parallelizes across different heuristics with clause sharing. Figure out the best heuristics. Get at least 4x speedup on 8 threads. Hope to Achieve: Get a working parallel implementation that parallelizes across the assignment space or clauses. Get at least 7x speedup on 8 threads. Win a SAT solver competition. Hope to Achieve if Things Go South: Successfully implement the algorithm sequentially; Get a working parallel implementation that parallelizes across different heuristics.
Platform Choice:
We have familiarity with OpenMP, OpenMPI, and CUDA. We didn’t think massive parallelism would be effective here because there isn’t a lot of opportunity for many threads in a warp to execute in lockstep as there is a lot of branching and sequential instructions. Additionally, we felt that OpenMPI might suffer more from more frequent clause sharing than OpenMP would. This is because each time you clause share with MPI, it would result in more interconnect traffic. With OpenMP, however, it would require an atomic change to a shared array. Both represent scalability constraints, but we felt our odds were better without explicit message passing to be able to optimize heavily.
Schedule:
Week 1: working sequential implementation Week 2: working parallel implementation w/o clause sharing Week 3: add clause sharing Week 4: at least 4x speedup on 8 threads Week 5: further optimize + parallelize across assignment space
Milestone Report:
Make sure project schedule is on track from initial proposal (P) Create a much more detailed timeline with half-week increment tasks each assigned to one person Put this on website (M, cause i cant edit the website)
Here was our original schedule:
Week 1: working sequential implementation
Week 2: working parallel implementation w/o clause sharing
Week 3: add clause sharing
Week 4: at least 4x speedup on 8 threads
Week 5: further optimize + parallelize across assignment space
We are at the midpoint of week 3, and we have completed the tasks we noted needed to be completed in Weeks 1 and 2. We are not close to fully implementing clause sharing and anticipate it will take longer than initially expected. Here is our updated timeline for the remainder of the semester that accounts for this:
Week 3-3.5: Devise plan for implementing clause sharing (pseudocode) (P)
Week 3.5-4: Modify actual code to implement clause sharing (P)
Week 4-4.5: Finish adding clause sharing (working through kinks and bugs) (M)
Week 4.5-5: Test speedup with just parallelization across heuristics (P) Test speedup with added clause sharing (M)
Week 5-5.5: Performance debug as much as possible to achieve the best speedup (P and M)
Week 5.5-6: Spend all remaining time preparing physical poster for Final project presentation on May 1, 2026 (P and M)
Write what work we have done so far in a couple of paragraphs (P)
Firstly, we have implemented a from-scratch CaDiCaL sequential algorithm that acts according to the following procedure:
The solver first scans the input formula to identify any unit propagation that can immediately occur (due to unit clauses) and conflicts that arise as a result
The solver enters the main CDCL loop
It guesses the assignment of unassigned variable(s) according to a heuristic
It uses watch pointers to identify the impacts of this new assignment on the value of other variables (unit propagation)
If any of these propagations lead to the formula evaluating to false, conflict resolution takes place
In conflict resolution, the algorithm learns what variable assignment kick-started the propagation that led to the conflict
It undoes assignments until right before that point and learns a clause that prevents that assignment from occurring again
It continues from that point
Then, we developed a working parallel version in which several threads run the algorithm simultaneously. They each proceed according to the procedure above. The only difference between the threads is that each uses a different heuristic to search the assignment space; the idea is that this increases the probability that one heuristic gets lucky and quickly finds a valid set of inputs. The parallel version uses the OpenMP API to spawn and manage threads.
Say how we believe we are doing with our goals we stated in the proposal (P)
Write a new, updated list of goals
Our original goals:
Plan to Achieve
Successfully implement the algorithm sequentially
Get a working implementation that parallelizes across different heuristics with clause sharing
Figure out the best heuristics
Get at least 4x speedup on 8 threads
Hope to Achieve
Get a working parallel implementation that parallelizes across the assignment space or clauses
Get at least 7x speedup on 8 threads
Win a SAT solver competition
Hope to Achieve if Things Go South
Successfully implement the algorithm sequentially
Get a working implementation that parallelizes across different heuristics
The “Hope to Achieve if Things go South” goals are already 100% complete. We have already completed the sequential implementation part of the “Plan to Achieve" goals. We should be on track to implement clause sharing as well. However, after doing additional research, we are no longer sure about 4x speedup as a reasonable goal for an 8 thread parallel CDCL implementation. This of course also calls into doubt our 7x speedup “Hope to Achieve” goal.
Here is an updated list of goals:
Hope to Achieve
3x parallel implementation speedup on 8 threads
Find a more efficient means of parallelization than heuristics + clause sharing
Plan to Achieve
2x parallel implementation speedup on 8 threads
Implement clause sharing across threads running different heuristics
Write about what we plan to have during the poster session (M)
We will have one paper in the center saying our names and our project title and a brief description of our project (what a SAT solver is and why its hard to parallelize)
We will have a paper that has on it a generated visualization (a decision tree or something) of the algorithm learning clauses and searching the assignment space
We will have a paper explaining our parallelization strategies and the performance debugging tricks we used to achieve a higher speedup
We plan to have graphs showing speedup vs the sequential implementation for parallelism with just parallelization across heuristics, and another with clause-sharing.
List most concerning issues currently (M)
The most concerning issue is that we haven’t done any performance measurements yet, so we have no idea how far off we are from our target of 2x speedup. Furthermore, we’re not sure how to implement clause sharing yet.
Final Project Report
Pranav Tatavarti, Michael Liang
Summary
Any boolean expression can be re-expressed as a conjunction of disjunctive clauses (CNF). We implemented a CDCL SAT Solver, an algorithm that attempts to determine whether a given CNF can be satisfied and, if so, what inputs satisfy it. Using C++ OpenMP on a multicore CPU, we parallelized a homemade CDCL implementation and achieved up to a 10x speedup on large inputs.
Background
CDCL Algorithm Flowchart.
The CDCL algorithm proceeds based on the following pseudocode:
The solver first scans the input formula to identify any immediate deductions (due to single variable clauses) and returns false if a conflict arises as a result
The solver enters the main CDCL loop
It guesses the assignment of unassigned variable(s) according to a heuristic
If there are no more unassigned variables, it returns the assignment
It uses watch pointers to identify the impacts of this new assignment on the value of other variables (unit propagation)
If any of these propagations lead to the formula evaluating to false, conflict resolution takes place
In conflict resolution, the algorithm learns a new clause that prevents the falsification of the formula which occurred
If the learned clause is empty, it returns unsatisfiable
It figures out what variable assignment kick-started the propagation that led to the conflict
It undoes assignments until right before that point
It continues from that point
To track all variable assignments, a vector of custom structs is used. Each instance of the struct contains information about each variable necessary for bookkeeping. Compared to several individual vectors for each field, packaging them into a struct enhances locality.
Our Boolean formula is stored as a vector of individual clauses, where each clause is a vector of individual literals. Literals are represented by either positive or negative versions of their variable numbers, depending on whether the literal contains a negation or not. (e.g. -1 represents the negation of variable 1). A variable number is simply its index into the assignment vector (variable 5 can be accessed at index 5).
As mentioned above, unit propagation occurs when an assignment forces another variable to hold a particular value. This occurs when all but 1 literal in a clause becomes falsified, forcing the remaining literal to be true. The naive way of performing unit propagation would be to linearly scan every clause, searching for clauses where one variable is left unassigned. To speed this up, we always make sure that if there are unassigned variables in a clause, they fill the first two positions.
Diagram illustrating the watch pointer data structure.
Additionally, so that we don’t have to iterate through our whole formula to find the clauses that involve a particular literal, we used a watch_pointer data structure. This is a 2D vector indexed by all possible literals we can have in our formula (num_variables * 2 in length). At each index, a list of clauses watching that literal is maintained.
The last critical data structure is ass_order, a queue implemented as a C++ vector that remembers all the variables we have updated. In unit propagation, this queue is used to determine which variables have changed, and thus which clauses to inspect for further changes (using the watch_pointers data structure).
There is very little independent work in this algorithm, as each individual step within the main loop depends on the previous step, and later iterations of the loop also depend on previous ones. As a result, we implemented portfolio parallelism. Each thread runs the algorithm with its own copy of the formula and assignment, and each runs a slightly different flavor of the VSIDS heuristic. VSIDS increases the weight on a variable each time it is involved in a conflict, increasing the likelihood it is chosen for assignment in the decision-making phase of the algorithm.
Temporal locality naturally emerges in this algorithm because of this heuristic, as VSIDS selects variables for assignment that have been involved in recent conflicts. Spatial locality is not great with CDCL due to severe pointer chasing. The flow of the algorithm repeatedly accesses random vectors that aren’t guaranteed to be near each other in memory. However, this was mitigated through our various optimizations, as we will explain.
Approach
We used C++ with OpenMP for the main algorithm, plus a combination of Python and ChatGPT to generate test cases. All of our programming and testing was done on the GHC machines. We first implemented a fully sequential algorithm, which was then parallelized and iteratively improved upon.
As mentioned previously, we parallelized across heuristics for the decision-making phase of our algorithm. The underlying idea was that with more flavors, the probability that one is well-suited to a given input is higher. Examples of parameters that were varied between different threads were the weighting factor VSIDS used and epsilon (the probability that VSIDS is abandoned, and a random variable is chosen instead).
Diagram illustrating portfolio parallelism
We then implemented clause sharing, where whenever a thread learned a new clause, it would share it with the other threads. We did this by maintaining a shared buffer vector that each thread would write learned clauses to. Each of the mentioned data structures in the background section has its own copy independently maintained by a single thread. The only shared data structure was this buffer. Adding to the shared buffer upon clause discovery and reading from the shared buffer at the beginning of each main loop iteration were the only changes made to the algorithm for the sake of parallelism.
The initial version of code that worked this way had abysmal parallel speedup, as the following graphs illustrate.
Single-threaded performance was often better than multi-threaded performance. Through analysis using the Linux perf tool built in on the GHC machines, 98% of the computation time was spent in the unit propagation phase of the algorithm on the php_10_9.txt test case with 8 threads. Very little time was spent in synchronization, which was expected. The primary driver of disproportionate unit prop time is having too many clauses, as this will force the algorithm to iterate longer per falsified variable. Thus, sharing a clause came at a computational cost. We decided it should only happen when there was reason to believe it would speed up a thread’s computation by forcing the assignment of variables. Shorter clauses are much more likely to do this than longer clauses. So, we started only sharing clauses of length 8 or less.
We were now achieving much greater levels of speedup, up to around 2x on 8 threads for our two larger test cases. Our intuition was correct, and we were importing far too many useless clauses that did nothing but clog our computations. The next round of perf analysis revealed that we were still dominated by unit propagation, this time at a mitigated 80%. This made visible secondary bottlenecks, which primarily were expensive O(N^2) clause scanning helper functions called multiple times throughout our algorithm.
We next applied a similar clause-limiting optimization locally. This was a local clause deletion, where whenever the number of conflicts exceeded a certain limit, and the formula exceeded a certain size, we deleted any learned clause with size greater than 8 that had not forced any variable assignments. This, along with speedier helper functions, resulted in the following speedup curve.
Our largest test case experienced over 3x speedup on 8 threads now. One plausible explanation is that this pruned the size of local thread copies of the boolean CNF formula, increasing the share of it that could fit within a cache and thus boosting locality, on top of speeding up unit propagation.
Another round of perf analysis revealed a brand-new bottleneck: 7.23% of computation time was spent on our resolve function, which was responsible for generating a new clause upon the algorithm encountering a conflict. It was needlessly written to be O(N^2). After fixing that, times got better for all thread counts, but speedup actually decreased because the change disproportionately impacted single-threaded performance compared to multi-thread performance.
Our algorithm was still faster for the end user this way, so we kept this optimization in. It illustrated that the application was more memory-bound and less compute-bound as the number of threads was increased.
To address this exact problem of slow memory accesses, we executed the following fixes:
Getting rid of a shared buffer_idxs array and using a local offset instead (this array was used by each thread to know where to begin reading into the shared buffer to import clauses)
Each thread only cares about its own offset anyway
Limits interconnect traffic by decreasing cache misses
Modification of the watch pointers data structure
Our data structure was vector<vector<int>>, where each inner vector was a list of clause indices in the formula vector that watched a certain literal. We changed that to vector<vector<custom struct>>. The custom struct added a field that stored the second literal that a given clause was watching.
During unit propagation, a variable is popped off the queue that tracks all recently falsified variables. The algorithm needs to evaluate the downstream impacts of this variable change, so it loops through all clauses that have watch pointers attached to that literal. To deduce whether this clause will force a new variable assignment, the algorithm needs to check the other literal that each clause is watching, aside from the one that was popped off the queue. To do this, the formula and clause vectors must be accessed. These live in totally different segments of memory than the queue or assignment vectors. Thus, a cache miss is pretty much guaranteed. The aforementioned modification causes the other literal that each clause watches to be pulled into the cache as soon as the watch pointer data structure is accessed, boosting locality.
This was our final optimization, and the results are discussed below.
Results
We defined our performance based on parallel speedup and wall-clock time. Given that large CNFs are incredibly tedious to write by hand, we had to use ChatGPT to generate multi-thousand-line CNF examples that fit the general patterns of real SAT solver use cases, like hardware verification, for instance. Underlying mathematical principles like graph coloring and the pigeonhole principle are often used as the backbone to easily grow these CNFs.
The final version of our code performed as follows:
These speedup graphs are generated in comparison to a baseline instance of our program running on a single thread. Each of these graphs is running identical configurations. The only difference is the test case.
A ranking of the test cases by size from longest to smallest is:
Coloring_mycielski_47nodes_5colors_unsat (last graph)
Mixed_coloring_60nodes_4colors
Xor_sat_180v_260eq_k4_seed42
Php_10_9
Length_three_1
Problem size certainly played a role. We excluded some test cases from our results section on the basis that they were far too small for parallelism to be meaningful. However, there were still large test cases that were negatively impacted by parallelism. This is because CDCL is suited for Boolean formulas that naturally occur in human work, like designing computer hardware or routing flights across airports. Such formulas are naturally structured to allow for rapid deduction. A few learned clauses can prune massive segments of the assignment space and save tons of work. This also leads to better multi-threaded speedup because it magnifies the impact of clause sharing.
Some test case generation methods, like the pigeonhole principle, naturally lend themselves to this, which is why we achieved solid speedup on them. However, test cases like xor_sat_180v_260eq_k4_seed42, a cryptographic benchmark specifically designed to limit information deduction, or mixed_coloring_60nodes_4colors, which is based on a large, completely random graph, work against this inductive bias. Those test cases received 1.63 and 0.63 8-thread speedup, respectively, compared to 3.02 with the php_10_9 test case. Adding more threads to them hardly benefited execution time and only made synchronization overhead more prominent.
Another property of a test case that can lead to positive speedup is when, of the many paths through the assignment space the algorithm can traverse, the majority lead the algorithm down a long chain that leads nowhere, but a very small subset will lead to a satisfiable solution very quickly. This perfectly lends itself to portfolio parallelism, as the probability of the fast paths being traversed gets far higher when many threads are independently searching the assignment space. Also, threads will disqualify the many slow paths faster because of clause sharing. This often leads to superlinear speedup, as seen with the coloring_mycielski_47nodes_5colors_unsat test case.
The CDCL algorithm’s nature was our fundamental limitation. It is so sequential that it can only be parallelized using portfolio parallelism. As we have seen, the effectiveness of that paradigm completely depends on the characteristics of the input problem.
The only point of synchronization in our program was when threads write to the shared buffer to perform clause sharing. As brought up in our approach section, mitigating the slowdown brought about massive performance improvements. As a result, synchronization time wasn’t the primary concern. At higher thread counts, as mentioned earlier, we are more bound by memory speed. This is somewhat inevitable for CDCL. A possible optimization that could have alleviated this was flattening our formula representation to a 1D vector to improve locality. We didn’t proceed with this for two reasons: 1. It would be a major upheaval, and we had no time left. 2. With a large enough test case, adjacent active clauses will likely not be in the same cache line due to clause deletion, putting a damper on the locality benefit, unless you manually shift all clauses that come later in the formula when deleting one, which is time-consuming.
We stand by our decision to use the GHC machines and multi-core CPUs. Massive parallelism on a GPU wouldn’t have helped because there was no way to exploit 32 threads in a warp executing in lockstep due to the algorithm.
References
ChatGPT, for generating test cases
https://www.cs.cmu.edu/~mheule/15311-s26/slides/CDCL.pdf, Professor Marijn J.H. Heule’s lecture slides contain a pseudocode blueprint for the CDCL algorithm that we used. They are part of his 15-311 course on Logic and Mechanized Reasoning
Work by each student
Phase 1 – Ideation and sequential implementation: Pranav - 50%, Michael - 50%
Brainstorming: Pranav 40%, Michael 60%
Solve function (implementing overall pseudocode) – Pranav
Learn function – Michael
Backtrack function – Michael
UnitProp function – Pranav
Debugging Sequential implementation - Pranav 50%, Michael 50%
Phase 2 – Parallelization of sequential implementation – 90% Pranav, 10% Michael
Developing pseudocode – Pranav 50%, Michael 50%
Setting up OpenMP on version w/o clause sharing – Michael
Implementing clause sharing - Pranav 90%, Michael 10%
Debugging parallel implementation - Pranav
Phase 3 – Optimization/Performance Debugging – Pranav
Implementing clause sharing filters – Pranav
Implementing local clause filtering – Pranav
Rewriting learn helper functions – Pranav
Rewriting resolve function – Pranav
Phase 4 – Writing the report - Pranav 90%, Michael 10%
60% Pranav, 40% Michael