mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

Update PARALLEL_PROJECT_NOTES.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-26 17:44:29 -07:00 • committed by GitHub
parent 9d0a2ae355
commit a9b4e35938
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
PARALLEL_PROJECT_NOTES.md
View file

@ -27,7 +27,7 @@ and possibly
* Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first.
* VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT).
* VSIDS does not keep track of variable phases (if the variable was set to true or false). * VSIDS does not keep track of variable phases (if the variable was set to true or false).
* Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial, slide 64 on Variable Scoring Schemes](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf)
* Proof prefix: * Proof prefix:
* Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score.
* The weight function can be formulated to take into account clause sizes. * The weight function can be formulated to take into account clause sizes.