SAT-bench -B 2971

shnarazk · Sep 20, 2024 · a9744ff · a9744ff
1 parent 84f0ce2
commit a9744ff
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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;