From f6ec7f53811f0d7bbfbfbcac2bc2b453bb19b45b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:03:52 -0700 Subject: [PATCH] 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