From 202807b3178333d3930922f4ca63650dd9d22f92 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 15:09:03 -0700 Subject: [PATCH] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 34c8b4314..1ce55e410 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -44,4 +44,26 @@ We track notes for updates to smt\_parallel.cpp and possibly solver/parallel\_ta This section considers various possible algorithms. +In the following, $F$ refers to the original goal, $T$ is the number of CPU cores or CPU threads. + +### Base algorithm + +The existing algorithm in smt_parallel is as follows: + +1. Run a solver on $F$ with a bounded number of conflicts. +2. If the result is SAT/UNSAT, or UNKNOWN with an interrupt or timeout, return. If the maximal number of conflicts were reached continue. +3. Spawn $T$ solvers on $F$ with a bounded number of conflicts, wait until a thread returns UNSAT/SAT or all threads have reached a maximal number of conflicts. +4. Perform a similar check as in 2. +5. Share unit literals learned by each thread. +6. Compute unit cubes for each thread $T$. +7. Spawn $T$ solvers with $F \wedge \ell$, where $\ell$ is a unit literal determined by lookahead function in each thread. +8. Perform a similar check as in 2. +9. Shared unit literals learned by each thread, increase the maximal number of conflicts, go to 3. + +### Algorithm Variants + +* Instead of using lookahead solving to find unit cubes use the proof-prefix based scoring function. +* Instead of using independent unit cubes, perform a systematic (where systematic can mean many things) cube and conquer strategy. +* Change the synchronization barrier discipline. +* [Future] Include in-processing