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

add notes on parameter tuning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-12 14:58:58 -07:00
parent 9e00b4b813
commit 49056db676
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

@ -140,7 +140,7 @@ The initial values of reward functions is fixed (to 1) and the initial values of
* The batch manager maintains a set of candidate parameters $CP = \{ (P_1, r_1), \ldots, (P_n, r_n) \}$. * The batch manager maintains a set of candidate parameters $CP = \{ (P_1, r_1), \ldots, (P_n, r_n) \}$.
* A worker thread picks up a parameter $P_i$ from $CP$ from the batch manager. * A worker thread picks up a parameter $P_i$ from $CP$ from the batch manager.
* It picks one or more parameter settings within $P_i$ whose mutation function have non-zero reward functions and applies a mutation. * It picks one or more parameter settings within $P_i$ whose mutation function have non-zero reward functions and applies a mutation.
* It then runs with a bounded set of cubes. * It then runs with a batch of cubes.
* It measures the reward for the new parameter setting based in number of cubes, cube depth, number of timeouts, and completions with number of conflicts. * It measures the reward for the new parameter setting based in number of cubes, cube depth, number of timeouts, and completions with number of conflicts.
* If the new reward is an improvement over $(P_i, r_i)$ it inserts the new parameter setting $(P_i', r_i')$ into the batch manager. * If the new reward is an improvement over $(P_i, r_i)$ it inserts the new parameter setting $(P_i', r_i')$ into the batch manager.
* The batch manager discards the worst parameter settings keeping the top $K$ ($K = 5$) parameter settings. * The batch manager discards the worst parameter settings keeping the top $K$ ($K = 5$) parameter settings.