mcsat heuristic update -- use similar heuristic parameters as in cdclt (

#506)
SRI-CSL · Apr 7, 2024 · 184a969 · 184a969
1 parent e7292fd
commit 184a969
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c
@@ -128,7 +128,7 @@ void bool_plugin_heuristics_init(bool_plugin_t* bp) {
 
   // Clause database compact
   bp->heuristic_params.lemma_limit_init = 1000;
-  bp->heuristic_params.lemma_limit_factor = 1.1;
+  bp->heuristic_params.lemma_limit_factor = 1.05;
 
   // Bool var scoring
   bp->heuristic_params.bool_var_bump_factor = 5;

diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
@@ -330,8 +330,8 @@ static
 void mcsat_heuristics_init(mcsat_solver_t* mcsat) {
   mcsat->heuristic_params.restart_interval = 10;
   mcsat->heuristic_params.lemma_restart_weight_type = LEMMA_WEIGHT_SIZE;
-  mcsat->heuristic_params.random_decision_freq = 0;
-  mcsat->heuristic_params.random_decision_seed = 0;
+  mcsat->heuristic_params.random_decision_freq = 0.02;
+  mcsat->heuristic_params.random_decision_seed = 0xabcdef98;
 }
 
 static