From 184a9695a6584c144d7cc8c42ff69a49a06da485 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Sun, 7 Apr 2024 14:59:01 -0700
Subject: [PATCH] mcsat heuristic update -- use similar heuristic parameters as
 in cdclt (#506)

---
 src/mcsat/bool/bool_plugin.c | 2 +-
 src/mcsat/solver.c           | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c
index f37aece2a..5106a4d82 100644
--- 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
index f097301d5..143dcfe4c 100644
--- 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