From a9744ff77baeddf14839ee87a8f44b1bb894113e Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 20 Sep 2024 16:02:12 +0900
Subject: [PATCH] SAT-bench -B 2971

---
 src/solver/search.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/search.rs b/src/solver/search.rs
index 5afcb2c4f..37f9e6c29 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -526,7 +526,7 @@ impl SolveIF for Solver {
                             let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
                             let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow();
                             // Note: val can be inf. It got better results.
-                            let val: f64 = 0.5 * ent.min(lbd) + ent.max(lbd) / n.sqrt();
+                            let val: f64 = 0.5 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2();
                             state.reduction_threshold = val;
                             cdb.reduce(asg, val);
                             ss.num_reduction += 1;