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

Update PARALLEL_PROJECT_NOTES.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-25 20:02:37 -07:00 • committed by GitHub
parent e1eb3ace3c
commit 82b4c3ea23
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
PARALLEL_PROJECT_NOTES.md
View file

@ -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 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. 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. 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 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. 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 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$, $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. 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.
#### Batching
Threads can work on more than one cube in a batch.