mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

Update PARALLEL_PROJECT_NOTES.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-17 18:51:38 -07:00 • committed by GitHub
parent 53f32bf08f
commit f7370466f0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
PARALLEL_PROJECT_NOTES.md
View file

@ -282,12 +282,14 @@ Ideas for other knobs that can be tested
<li> Replace backoff scheme by a geometric scheme: add <b>conflict_inc</b> (a new parameter) every time and increment <b>conflict_inc</b>.</li>
<li> Revert backoff if a cube is solved.</li>
<li>Delay lemma and unit sharing.</li>
<li>Vary <b>max_cube_size</b>, or add a parameter to grow <b>max_cube_size</b> if initial attempts to conquer reach <b>max_conflicts</b>.</li>
</il>
<pre>
cube_initial_only (bool) (default: false) only useful when never_cube=false
frugal_cube_only (bool) (default: false) only useful when never_cube=false
max_conflict_mul (double) (default: 1.5)
max_cube_size (unsigned int) (default: 20) only useful when never_cube=false
never_cube (bool) (default: false)
relevant_units_only (bool) (default: true) only useful when share_units=true
share_conflicts (bool) (default: true) only useful when never_cube=false