From 138ac63dd054bab8f65e5fbaca52127dd2f37a64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 11:23:05 -0700 Subject: [PATCH 01/15] added notes Signed-off-by: Nikolaj Bjorner --- PARALLEL_PROJECT_NOTES.md | 49 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 PARALLEL_PROJECT_NOTES.md diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md new file mode 100644 index 000000000..4beb01265 --- /dev/null +++ b/PARALLEL_PROJECT_NOTES.md @@ -0,0 +1,49 @@ +\# Parallel project notes + + + +We track notes for updates to smt\_parallel.cpp and possibly solver/parallel\_tactic.cpp + + + + + +\## Variable selection heuristics + + + +* Lookahead solvers: + \* lookahead in the smt directory performs a simplistic lookahead search using unit propagation. + \* lookahead in the sat directory uses custom lookahead solver. + They both proxy on a cost model where the most useful variable to branch on is the one that \_minimizes\_ the set of new clauses maximally + through unit propagation. In other words, if a literal \_p\_ is set to true, and \_p\_ occurs in clause $\\neg p \\vee q \\vee r$, then it results in + reducing the clause from size 3 to 2 (because $\\neg p$ will be false after propagating \_p\_). +* VSIDS: + +  \* As referenced in Matteo and Antti's solvers. + \* Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. + \* VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). + \* VSIDS does not keep track of variable phases (if the variable was set to true or false). + +* Proof prefix: + \* Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. + \* The weight function can be formulated to take into account clause sizes. + \* The score assignment may also decay similar to VSIDS. + \* We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. +* From local search: + \* Note also that local search solvers can be used to assign variable branch priorities. + \* We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. + \* The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. + \* Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. +* Assignment trails: + \* We could also consider the assignments to variables during search. + \* Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. + \* The cubes resulting from such variables might be a direction towards finding satisfying solutions. + + +\## Algorithms + + + +This section considers various possible algorithms. + From e732354259333d0e54d8bed85608a09351fd6316 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 15:00:32 -0700 Subject: [PATCH 02/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 44 +++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 23 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 4beb01265..34c8b4314 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -1,4 +1,4 @@ -\# Parallel project notes +# Parallel project notes @@ -8,40 +8,38 @@ We track notes for updates to smt\_parallel.cpp and possibly solver/parallel\_ta -\## Variable selection heuristics +## Variable selection heuristics * Lookahead solvers: - \* lookahead in the smt directory performs a simplistic lookahead search using unit propagation. - \* lookahead in the sat directory uses custom lookahead solver. + * lookahead in the smt directory performs a simplistic lookahead search using unit propagation. + * lookahead in the sat directory uses custom lookahead solver. They both proxy on a cost model where the most useful variable to branch on is the one that \_minimizes\_ the set of new clauses maximally through unit propagation. In other words, if a literal \_p\_ is set to true, and \_p\_ occurs in clause $\\neg p \\vee q \\vee r$, then it results in reducing the clause from size 3 to 2 (because $\\neg p$ will be false after propagating \_p\_). -* VSIDS: - -  \* As referenced in Matteo and Antti's solvers. - \* Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. - \* VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). - \* VSIDS does not keep track of variable phases (if the variable was set to true or false). - +* VSIDS: + * As referenced in Matteo and Antti's solvers. + * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. + * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). + * VSIDS does not keep track of variable phases (if the variable was set to true or false). * Proof prefix: - \* Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. - \* The weight function can be formulated to take into account clause sizes. - \* The score assignment may also decay similar to VSIDS. - \* We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. + * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. + * The weight function can be formulated to take into account clause sizes. + * The score assignment may also decay similar to VSIDS. + * We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. * From local search: - \* Note also that local search solvers can be used to assign variable branch priorities. - \* We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. - \* The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. - \* Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. + * Note also that local search solvers can be used to assign variable branch priorities. + * We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. + * The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. + * Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. * Assignment trails: - \* We could also consider the assignments to variables during search. - \* Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. - \* The cubes resulting from such variables might be a direction towards finding satisfying solutions. + * We could also consider the assignments to variables during search. + * Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. + * The cubes resulting from such variables might be a direction towards finding satisfying solutions. -\## Algorithms +## Algorithms From 202807b3178333d3930922f4ca63650dd9d22f92 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 15:09:03 -0700 Subject: [PATCH 03/15] 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 From f6fc5045d21bae4a68219980659d6372c461364f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 15:12:13 -0700 Subject: [PATCH 04/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 1ce55e410..cdce9cd7d 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -15,9 +15,9 @@ We track notes for updates to smt\_parallel.cpp and possibly solver/parallel\_ta * Lookahead solvers: * lookahead in the smt directory performs a simplistic lookahead search using unit propagation. * lookahead in the sat directory uses custom lookahead solver. - They both proxy on a cost model where the most useful variable to branch on is the one that \_minimizes\_ the set of new clauses maximally - through unit propagation. In other words, if a literal \_p\_ is set to true, and \_p\_ occurs in clause $\\neg p \\vee q \\vee r$, then it results in - reducing the clause from size 3 to 2 (because $\\neg p$ will be false after propagating \_p\_). + They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally + through unit propagation. In other words, if a literal _p_ is set to true, and _p_ occurs in clause $\neg p \vee q \vee r$, then it results in + reducing the clause from size 3 to 2 (because $\neg p$ will be false after propagating _p_). * VSIDS: * As referenced in Matteo and Antti's solvers. * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. @@ -57,7 +57,7 @@ The existing algorithm in smt_parallel is as follows: 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. +8. Perform a similar check as in 2. But note that a thread can be UNSAT because the unit cube $\ell$ contradicted $F$. In this case learn the unit literal $\neg \ell$. 9. Shared unit literals learned by each thread, increase the maximal number of conflicts, go to 3. ### Algorithm Variants From 9bba708f9b34300be3e1252b3948549b5eec1e20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 15:36:37 -0700 Subject: [PATCH 05/15] fix compilation Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 2 +- src/smt/smt_internalizer.cpp | 7 ++++--- src/smt/smt_parallel.cpp | 3 +++ 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index da6e92569..352ea7111 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -189,7 +189,7 @@ namespace smt { unsigned_vector m_lit_occs; //!< occurrence count of literals svector m_bdata; //!< mapping bool_var -> data svector m_activity; - svector m_scores; + svector m_scores[2]; clause_vector m_aux_clauses; clause_vector m_lemmas; vector m_clauses_to_reinit; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index faf7ea24d..9a04741e2 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -928,8 +928,9 @@ namespace smt { set_bool_var(id, v); m_bdata.reserve(v+1); m_activity.reserve(v+1); - m_scores.reserve(v + 1); - m_scores[v][0] = m_scores[v][1] = 0.0; + m_scores[0].reserve(v + 1); + m_scores[1].reserve(v + 1); + m_scores[0][v] = m_scores[1][v] = 0.0; m_bool_var2expr.reserve(v+1); m_bool_var2expr[v] = n; literal l(v, false); @@ -1531,7 +1532,7 @@ namespace smt { for (unsigned i = 0; i < n; ++i) { auto lit = lits[i]; unsigned v = lit.var(); - m_scores[v][lit.sign()] += 1.0 / n; + m_scores[lit.sign()][v] += 1.0 / n; } } diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index ac5a81979..8e07ed492 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -92,6 +92,9 @@ namespace smt { sl.push_child(&(new_m->limit())); } + // Access socres as follows: + // ctx.m_scores[lit.sign()][lit.var()] + // auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) { // lookahead lh(ctx); // c = lh.choose(); From f2ff0adc791b8ddc711af5b23b7884b4fafc61be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 15:52:46 -0700 Subject: [PATCH 06/15] more notes Signed-off-by: Nikolaj Bjorner --- PARALLEL_PROJECT_NOTES.md | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index cdce9cd7d..320d8631d 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -64,6 +64,43 @@ The existing algorithm in smt_parallel is as follows: * 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. +* Spawn some threads to work in "SAT" mode, tuning to find models instead of short resolution proofs. * Change the synchronization barrier discipline. * [Future] Include in-processing +### Cube and Conquer strategy + +We could maintain a global decomposition of the search space by maintaing a list of _cubes_. +Initially, the list of cubes has just one element, the cube with no literals $[ [] ]$. +By using a list of cubes instead of a _set_ of cubes we can refer to an ordering. +For example, cubes can be ordered by a suffix traversal of the _cube tree_ (the tree formed by +case splitting on the first literal, children of the _true_ branch are the cubes where the first +literal is true, children of the _false_ branch are the cubes where the first literal is false). + +The main question is going to be how the cube decomposition is created. + +#### Static cubing +We can aim for a static cube strategy that uses a few initial (concurrent) probes to find cube literals. +This strategy would be a parallel implementaiton of proof-prefix approach. The computed cubes are inserted +into the list of cubes and the list is consumed by a second round. + +### Growing cubes on demand +Based on experiences with cubing so far, there is high variance in how easy cubes are to solve. +Some cubes will be harder than others to solve. For hard cubes, it is tempting to develop a recursive +cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level cubing. + +* The solver would have to identify hard cubes vs. easy cubes. +* It would have to know when to stop working on a hard cube and replace it in the list of cubes by + a new list of sub-cubes. + +* Ideally, we don't need any static cubing and cubing is grown on demand while all threads are utilized. + * If we spawn $T$ threads to initially work with empty cubes, we could extract up to $T$ indepenent cubes + by examining the proof-prefix of their traces. This can form the basis for the first, up to $2^T$ cubes. + * After a round of solving with each thread churning on some cubes, we may obtain more proof-prefixes from + _hard_ cubes. It is not obvious that we want to share cubes from different proof prefixes at this point. + But a starting point is to split a hard cube into two by using the proof-prefix from attempting to solve it. + +### Representing cubes implicitly and batching. + +* We can represent a list of cubes by using intervals and only represent start and end-points of the intervals. +* Threads can work on more than one cube in a batch. From e1eb3ace3ca0f7d0c152e91822777ed2a681d005 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 19:35:51 -0700 Subject: [PATCH 07/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 320d8631d..c280dc65a 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -98,7 +98,13 @@ cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level by examining the proof-prefix of their traces. This can form the basis for the first, up to $2^T$ cubes. * After a round of solving with each thread churning on some cubes, we may obtain more proof-prefixes from _hard_ cubes. It is not obvious that we want to share cubes from different proof prefixes at this point. - But a starting point is to split a hard cube into two by using the proof-prefix from attempting to solve it. + But a starting point is to split a hard cube into two by using the proof-prefix from attempting to solve it. + * Suppose we take the proof-prefix sampling algorithm at heart: It says to start with some initial cube prefix + and then sample for other cube literals. If we translate it to the case where multiple cubes are being processed + in parallel, then an analogy is to share candidates for new cube literals among cubes that are close to each-other. + For example, if thread $t_1$ processes cube $a, b, c$ and $t_2$ processes $a,b, \neg c$. They are close. They are only + separated by Hamming distance 1. If $t_1$ finds cube literal $d$ and $t_2$ finds cube literal $e$, we could consider the cubes + $a, b, c, d, e$, $a, b, c, d, \neg e$, $\ldots$, $a, b, \neg c, \neg d, \neg e$. ### Representing cubes implicitly and batching. From 82b4c3ea2321cd8811d766871821870ee91c3faf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:02:37 -0700 Subject: [PATCH 08/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index c280dc65a..7f35af8f0 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -84,7 +84,7 @@ We can aim for a static cube strategy that uses a few initial (concurrent) probe This strategy would be a parallel implementaiton of proof-prefix approach. The computed cubes are inserted into the list of cubes and the list is consumed by a second round. -### Growing cubes on demand +#### Growing cubes on demand Based on experiences with cubing so far, there is high variance in how easy cubes are to solve. Some cubes will be harder than others to solve. For hard cubes, it is tempting to develop a recursive cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level cubing. @@ -106,7 +106,9 @@ cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level separated by Hamming distance 1. If $t_1$ finds cube literal $d$ and $t_2$ finds cube literal $e$, we could consider the cubes $a, b, c, d, e$, $a, b, c, d, \neg e$, $\ldots$, $a, b, \neg c, \neg d, \neg e$. -### Representing cubes implicitly and batching. +#### Representing cubes implicitly -* We can represent a list of cubes by using intervals and only represent start and end-points of the intervals. -* Threads can work on more than one cube in a batch. +We can represent a list of cubes by using intervals and only represent start and end-points of the intervals. + +#### Batching +Threads can work on more than one cube in a batch. From f6ec7f53811f0d7bbfbfbcac2bc2b453bb19b45b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:03:52 -0700 Subject: [PATCH 09/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 7f35af8f0..5964037a7 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -104,7 +104,7 @@ cubing strategy. Ideally, a recursive cubing strategy is symmetric to top-level in parallel, then an analogy is to share candidates for new cube literals among cubes that are close to each-other. For example, if thread $t_1$ processes cube $a, b, c$ and $t_2$ processes $a,b, \neg c$. They are close. They are only separated by Hamming distance 1. If $t_1$ finds cube literal $d$ and $t_2$ finds cube literal $e$, we could consider the cubes - $a, b, c, d, e$, $a, b, c, d, \neg e$, $\ldots$, $a, b, \neg c, \neg d, \neg e$. + $a, b, c, d, e$, and $a, b, c, d, \neg e$, $\ldots$, $a, b, \neg c, \neg d, \neg e$. #### Representing cubes implicitly From 964363504ceca953c5d0aad72f657491707c80c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:13:06 -0700 Subject: [PATCH 10/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 5964037a7..4f1cff598 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -2,7 +2,7 @@ -We track notes for updates to smt\_parallel.cpp and possibly solver/parallel\_tactic.cpp +We track notes for updates to smt/parallel.cpp and possibly solver/parallel\_tactic.cpp @@ -112,3 +112,8 @@ We can represent a list of cubes by using intervals and only represent start and #### Batching Threads can work on more than one cube in a batch. + +### Synchronization + +* The first thread to time out or finish could kill other threads instead of joining on all threads to finish. +* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in sat/sat_parallel.cpp. From c3da87ca126e5cdc4e32a8f8c5710ed218a086d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:15:29 -0700 Subject: [PATCH 11/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 4f1cff598..36ff74d15 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -2,7 +2,10 @@ -We track notes for updates to smt/parallel.cpp and possibly solver/parallel\_tactic.cpp +We track notes for updates to +[smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) +and possibly +[https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactic.cpp](solver/parallel_tactic.cpp). @@ -116,4 +119,4 @@ Threads can work on more than one cube in a batch. ### Synchronization * The first thread to time out or finish could kill other threads instead of joining on all threads to finish. -* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in sat/sat_parallel.cpp. +* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in [sat/sat_parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_parallel.cpp) From 4c229d057dc728ac1e7b86e08cd43b8e5f3c0c01 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:16:12 -0700 Subject: [PATCH 12/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 36ff74d15..22e249960 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -5,7 +5,7 @@ We track notes for updates to [smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) and possibly -[https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactic.cpp](solver/parallel_tactic.cpp). +[solver/parallel_tactic.cpp](https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactic.cpp). From 27c1ffc7fb15850f08c20532a0a6c18930735733 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:17:19 -0700 Subject: [PATCH 13/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 22e249960..df7107c3d 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -5,7 +5,7 @@ We track notes for updates to [smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) and possibly -[solver/parallel_tactic.cpp](https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactic.cpp). +[solver/parallel_tactic.cpp](https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactical.cpp). From 9d0a2ae355e23f0d0312b12339d669b3dd4853ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Jul 2025 17:40:43 -0700 Subject: [PATCH 14/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index df7107c3d..88b521e96 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -17,35 +17,38 @@ and possibly * Lookahead solvers: * lookahead in the smt directory performs a simplistic lookahead search using unit propagation. - * lookahead in the sat directory uses custom lookahead solver. - They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally + * lookahead in the sat directory uses custom lookahead solver based on MARCH. March is described in Handbook of SAT and Knuth volumne 4. + * They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally through unit propagation. In other words, if a literal _p_ is set to true, and _p_ occurs in clause $\neg p \vee q \vee r$, then it results in reducing the clause from size 3 to 2 (because $\neg p$ will be false after propagating _p_). + * Selected references: SAT handbook, Knuth Volumne 4, Marijn's March solver on github, [implementation of march in z3](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_lookahead.cpp) * VSIDS: * As referenced in Matteo and Antti's solvers. * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). * VSIDS does not keep track of variable phases (if the variable was set to true or false). + * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) * Proof prefix: * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. * The weight function can be formulated to take into account clause sizes. * The score assignment may also decay similar to VSIDS. * We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. + * Selected references: [Battleman et al](https://www.cs.cmu.edu/~mheule/publications/proofix-SAT25.pdf) * From local search: * Note also that local search solvers can be used to assign variable branch priorities. * We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. * The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. * Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. + * Selected references: [Cai et al](https://www.jair.org/index.php/jair/article/download/13666/26833/) * Assignment trails: * We could also consider the assignments to variables during search. * Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. * The cubes resulting from such variables might be a direction towards finding satisfying solutions. + * Selected references: [Alex and Vadim](https://link.springer.com/chapter/10.1007/978-3-319-94144-8_7) and most recently [Robin et al](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9). ## Algorithms - - 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. From a9b4e35938483bce4ccd336442fd6927add42f3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Jul 2025 17:44:29 -0700 Subject: [PATCH 15/15] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 88b521e96..e9fcff91b 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -27,7 +27,7 @@ and possibly * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). * VSIDS does not keep track of variable phases (if the variable was set to true or false). - * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) + * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial, slide 64 on Variable Scoring Schemes](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) * Proof prefix: * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. * The weight function can be formulated to take into account clause sizes.