mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

Update PARALLEL_PROJECT_NOTES.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-17 18:08:23 -07:00 • committed by GitHub
parent 97d7723c44
commit a5c9e370de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
PARALLEL_PROJECT_NOTES.md
View file

@ -275,11 +275,13 @@ threads-4-cube-shareconflicts
Ideas for other knobs that can be tested
<il>
<li> Only cube on literals that exist in initial formula. Don't cube on literals created during search (such as by theory lemmas).
<li> Only share units for literals that exist in the initial formula.
<li> Vary the backoff scheme for <b>max_conflict_mul</b> from 1.5 to lower and higher.
<li> Vary <b>smt.threads.max_conflicts</b>
<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> Only cube on literals that exist in initial formula. Don't cube on literals created during search (such as by theory lemmas).</li>
<li> Only share units for literals that exist in the initial formula.</li>
<li> Vary the backoff scheme for <b>max_conflict_mul</b> from 1.5 to lower and higher.</li>
<li> Vary <b>smt.threads.max_conflicts</b>.</li>
<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>
</il>
<pre>