mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 20:21:23 +00:00
Code Activity

Update PARALLEL_PROJECT_NOTES.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-25 19:35:51 -07:00 • committed by GitHub
parent f2ff0adc79
commit e1eb3ace3c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
PARALLEL_PROJECT_NOTES.md
View file

@ -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.