Polarity driven rephasing 20260617

README.md

@@ -22,52 +22,52 @@ Though Splr comes with **ABSOLUTELY NO WARRANTY**, I'd like to show some results
 
 #### Version 0.19.0
 
-- (0.19.0-rc7) @ 2026-06-16T17:15:17
-
-| # | target CNF solved by splr                            |time (s)|ret|val|
-|--:|:-----------------------------------------------------|-------:|:-:|---|
-|  1|`04648cef5bed430ab6429991fa9e107d-ramsey_3_6_19.norma`|        |124|   |
-|  2|`0c0430a68f147be18ab3fded07f30fdb-oddball_53_5_tto_zp`|   36.19| 10|   |
-|  3|`0ccb0f855352783a972be45188bf3164-SCPC-500-12.cnf`    |  117.39| 20|   |
-|  4|`0e1d562093d5f4fc9013cf4a14a03f70-Break_12_50.xml.cnf`|    6.58| 10|   |
-|  5|`110f8eb8b9b80204fe955ea0973bbb00-clqcl_30_7_6.normal`|        |124|   |
-|  6|`24bde22f729a988fb2394b644cb60d39-SC25_Timetable_C_48`|   28.10| 10|   |
-|  7|`2d0c041c0fe72dc32527bfbf34f63e61-170223547.cnf`      |        |124|   |
-|  8|`35b9091b90bd28a492c9556d6fc4348d-bp4_TCO_CSO_ZR.norm`|        |124|   |
-|  9|`35ec95b9b2398fb522db178855016ae0-MVRoundRobin_n14_d1`|        |124|   |
-| 10|`46a8727e27d848faafd83a990c2e01a7-case8.normalised.cn`|        |124|   |
-| 11|`482295be38dc1d63a16f3cf649ef7ef6-myciel6-cn.used-as.`|        |124|   |
-| 12|`53c21f3e78f060883026b5a12ba691d8-maximum_constrained`|   14.32| 10|   |
-| 13|`57b478982ee9aba245ba792452b18fe3-VanDerWaerden_pd_2-`| 1559.81| 10|   |
-| 14|`6147e666b75f603a4c4490d21ab654cd-hid-uns-enc-6-1-0-0`|  432.30| 20|   |
-| 15|`65f7145996bbec02b90bd0fa64a20502-test_v7_r12_vr10_c1`|        |124|   |
-| 16|`68e33d998466bbdd4bfb7249a5790e4f-arles_thres10_p10_r`|    0.68| 20|   |
-| 17|`83aa254f7d17e1df7bee19322ac4752b-1.normalised.cnf`   |        |124|   |
-| 18|`8e62c5d47920ffe36052f86177403e70-SC25_Timetable_C_39`|   13.60| 10|   |
-| 19|`908433870bee8ba2c86f266d0b002fdb-MVRoundRobin_n20_d1`|        |124|   |
-| 20|`918d9e7c2e197312517736421d728958-SCPC-500-1.cnf`     |  235.12| 20|   |
-| 21|`91c429adc2dc8430461b6d87a9aef335-16_16_booth_wallace`|        |124|   |
-| 22|`967b58fea99a99b8da592d3e2fe7139b-dubois50.cnf.mis-99`|        |124|   |
-| 23|`98a9352230efc411c092f1dcdcdedcfc-bp4_BC012_IXA_LPI_F`|        |124|   |
-| 24|`9b5f767eb5c14eb888d51acf70e045c8-uniqinv40prop.cnf`  |        |124|   |
-| 25|`a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r`|    0.68| 20|   |
-| 26|`a1fdd60d2570f47fb14956ac9e96951f-oddball_22_5_ttf.no`|   32.42| 20|   |
-| 27|`a70883771fd1c210d94a916d52510a3a-gm28sparrc.cnf`     |   17.62| 20|   |
-| 28|`b3d3680b3287a989ce61a6db1054efd2-case20.normalised.c`|    5.46| 10|   |
-| 29|`b9ed6fd14f4fc969ec966a4b54c36872-n320p5q2_n.apx_16.c`|   19.50| 10|   |
-| 30|`c21096fa2f550785c33dc862d83bc941-case17.normalised.c`|   52.47| 10|   |
-| 31|`cb950b9accfb53eb98f77b0f995ac0ae-rphp5_050_shuffled.`|        |124|   |
-| 32|`d5928883c1e1f70764a31a83aa419eaf-oski15a01b42s_opt.c`| 1824.52| 20|   |
-| 33|`d8666a18cf3a32af0a606099f0070b4b-7.normalised.cnf`   |        |124|   |
-| 34|`ddf9620410e6a4351f64c745670ef5d4-oddball_57_5_tto_zp`|   62.92| 10|   |
-| 35|`e23edb67db2d1dfdbfe2f4c02d09c6c7-14.normalised.cnf`  |  495.46| 10|   |
-| 36|`e430acf720b63044e5c825a00a76b0eb-rphp_p25_r25.cnf`   |        |124|   |
-| 37|`e442248e155eb81a811edd1deca8a2cd-sudoku-N30-23.cnf`  |        |124|   |
-| 38|`f17dfbed8c18716a41b231702e127524-SC25_Timetable_C_40`|   12.37| 10|   |
-| 39|`f25a1df88f89c6bcbe2602fa7f6e816b-1-TC-256-K-63.sanit`| 2607.61| 10|   |
-| 40|`f33a6163305d6559043b7438a692dea9-simon-r17-1.sanitiz`|        |124|   |
-
-"splr"    , med:     32.42, max:   2607.61,total except 19 timeouts: 7575.10
+- (0.19.0-rc7) @ 2026-06-28T00:12:52
+
+| # | target CNF solved by splr                            |time (s)|ret|
+|--:|:-----------------------------------------------------|-------:|:-:|
+|  1|`04648cef5bed430ab6429991fa9e107d-ramsey_3_6_19.norma`|        |124|
+|  2|`0c0430a68f147be18ab3fded07f30fdb-oddball_53_5_tto_zp`|  929.05| 10|
+|  3|`0ccb0f855352783a972be45188bf3164-SCPC-500-12.cnf`    |  139.97| 20|
+|  4|`0e1d562093d5f4fc9013cf4a14a03f70-Break_12_50.xml.cnf`|   42.03| 10|
+|  5|`110f8eb8b9b80204fe955ea0973bbb00-clqcl_30_7_6.normal`|        |124|
+|  6|`24bde22f729a988fb2394b644cb60d39-SC25_Timetable_C_48`|  114.26| 10|
+|  7|`2d0c041c0fe72dc32527bfbf34f63e61-170223547.cnf`      |        |124|
+|  8|`35b9091b90bd28a492c9556d6fc4348d-bp4_TCO_CSO_ZR.norm`|        |124|
+|  9|`35ec95b9b2398fb522db178855016ae0-MVRoundRobin_n14_d1`|        |124|
+| 10|`46a8727e27d848faafd83a990c2e01a7-case8.normalised.cn`|        |124|
+| 11|`482295be38dc1d63a16f3cf649ef7ef6-myciel6-cn.used-as.`|        |124|
+| 12|`53c21f3e78f060883026b5a12ba691d8-maximum_constrained`|   42.53| 10|
+| 13|`57b478982ee9aba245ba792452b18fe3-VanDerWaerden_pd_2-`| 2360.11| 10|
+| 14|`6147e666b75f603a4c4490d21ab654cd-hid-uns-enc-6-1-0-0`|  830.97| 20|
+| 15|`65f7145996bbec02b90bd0fa64a20502-test_v7_r12_vr10_c1`|        |124|
+| 16|`68e33d998466bbdd4bfb7249a5790e4f-arles_thres10_p10_r`|    2.99| 20|
+| 17|`83aa254f7d17e1df7bee19322ac4752b-1.normalised.cnf`   |        |124|
+| 18|`8e62c5d47920ffe36052f86177403e70-SC25_Timetable_C_39`|   38.42| 10|
+| 19|`908433870bee8ba2c86f266d0b002fdb-MVRoundRobin_n20_d1`|        |124|
+| 20|`918d9e7c2e197312517736421d728958-SCPC-500-1.cnf`     |  172.92| 20|
+| 21|`91c429adc2dc8430461b6d87a9aef335-16_16_booth_wallace`|        |124|
+| 22|`967b58fea99a99b8da592d3e2fe7139b-dubois50.cnf.mis-99`|        |124|
+| 23|`98a9352230efc411c092f1dcdcdedcfc-bp4_BC012_IXA_LPI_F`|        |124|
+| 24|`9b5f767eb5c14eb888d51acf70e045c8-uniqinv40prop.cnf`  |        |124|
+| 25|`a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r`|    2.96| 20|
+| 26|`a1fdd60d2570f47fb14956ac9e96951f-oddball_22_5_ttf.no`|   38.66| 20|
+| 27|`a70883771fd1c210d94a916d52510a3a-gm28sparrc.cnf`     |    4.75| 20|
+| 28|`b3d3680b3287a989ce61a6db1054efd2-case20.normalised.c`|  378.93| 10|
+| 29|`b9ed6fd14f4fc969ec966a4b54c36872-n320p5q2_n.apx_16.c`|   29.64| 10|
+| 30|`c21096fa2f550785c33dc862d83bc941-case17.normalised.c`|  794.55| 10|
+| 31|`cb950b9accfb53eb98f77b0f995ac0ae-rphp5_050_shuffled.`|        |124|
+| 32|`d5928883c1e1f70764a31a83aa419eaf-oski15a01b42s_opt.c`|        |124|
+| 33|`d8666a18cf3a32af0a606099f0070b4b-7.normalised.cnf`   |        |124|
+| 34|`ddf9620410e6a4351f64c745670ef5d4-oddball_57_5_tto_zp`| 1148.32| 10|
+| 35|`e23edb67db2d1dfdbfe2f4c02d09c6c7-14.normalised.cnf`  |  619.00| 10|
+| 36|`e430acf720b63044e5c825a00a76b0eb-rphp_p25_r25.cnf`   |        |124|
+| 37|`e442248e155eb81a811edd1deca8a2cd-sudoku-N30-23.cnf`  |        |124|
+| 38|`f17dfbed8c18716a41b231702e127524-SC25_Timetable_C_40`| 1266.08| 10|
+| 39|`f25a1df88f89c6bcbe2602fa7f6e816b-1-TC-256-K-63.sanit`|  773.27| 10|
+| 40|`f33a6163305d6559043b7438a692dea9-simon-r17-1.sanitiz`|  117.68| 10|
+
+- "splr"    , med:    139.97, max:   2360.11,total except 19 timeouts: 9847.07
 
 #### Version 0.17.0
 

src/assign/learning_rate.rs

@@ -58,6 +58,10 @@ impl ActivityIF<VarId> for AssignStack {
         self.activity_stay_rate = 1.0 - scaling;
         self.activity_learning_rate = scaling;
     }
+    fn rescale_learning_rate(&mut self, scaling: f64) {
+        self.activity_learning_rate *= scaling;
+        self.activity_stay_rate = 1.0 - self.activity_learning_rate;
+    }
     // Note: `update_rewards` should be called before `cancel_until`
     #[inline]
     fn update_activity_tick(&mut self) {

src/assign/mod.rs

@@ -43,6 +43,8 @@ pub trait AssignIF:
 {
     /// return root level.
     fn root_level(&self) -> DecisionLevel;
+    /// return current conflict index.
+    fn current_conflict_index(&self) -> usize;
     /// return a literal in the stack.
     fn stack(&self, i: usize) -> Lit;
     /// return literals in the range of stack.

src/assign/propagate.rs

@@ -206,7 +206,7 @@ impl PropagateIF for AssignStack {
                 self.var[l.vi()].assign.is_some(),
                 "cancel_until found unassigned var in trail {}{:?}",
                 l.vi(),
-                &self.var[l.vi()],
+                self.var[l.vi()],
             );
             let vi = l.vi();
             #[cfg(feature = "trace_propagation")]
@@ -237,6 +237,8 @@ impl PropagateIF for AssignStack {
                 if cfg!(feature = "rephase")
                 // && self.num_conflict - v.last_conflict <= 1000
                 {
+                    v.polarity *= 0.999;
+                    v.polarity += 0.001 * if v.assign.unwrap() { 1.0 } else { -1.0 };
                     v.set(
                         FlagVar::PHASE,
                         match self.phase_mode {
@@ -246,10 +248,16 @@ impl PropagateIF for AssignStack {
                             RephaseTarget::Best => {
                                 self.best_phases[vi].0.unwrap_or(v.assign.unwrap())
                             }
-                            RephaseTarget::Random => {
-                                (v.last_conflict + i + self.num_propagation).is_multiple_of(2)
-                            }
+                            RephaseTarget::Random => self.rng.next_bool(),
                             RephaseTarget::Inverted => !v.assign.unwrap(),
+                            RephaseTarget::Polarity => {
+                                if self.rng.next_f64() <= v.polarity.abs().powf(1.2) {
+                                    v.assign.unwrap()
+                                } else {
+                                    !v.assign.unwrap()
+                                    // self.rng.next_f64() >= 0.5
+                                }
+                            }
                         },
                     );
                 } else {

src/assign/select.rs

@@ -14,6 +14,7 @@ pub enum RephaseTarget {
     True,
     Random,
     Inverted,
+    Polarity,
 }
 
 impl RephaseTarget {
@@ -26,6 +27,7 @@ impl RephaseTarget {
             RephaseTarget::True => "⊤",
             RephaseTarget::Random => "∼",
             RephaseTarget::Inverted => "¬",
+            RephaseTarget::Polarity => "φ",
         }
     }
 }
@@ -59,7 +61,8 @@ pub trait VarSelectIF {
     fn rebuild_order(&mut self);
     /// save the current assignments as the best phases.
     /// return the core size.
-    fn save_best_phases(&mut self) -> usize;
+    fn save_best_phases(&mut self, new_best: bool) -> usize;
+    fn clear_best_phases(&mut self);
 }
 
 impl VarSelectIF for AssignStack {
@@ -103,20 +106,32 @@ impl VarSelectIF for AssignStack {
             }
         }
     }
-    fn save_best_phases(&mut self) -> usize {
+    fn save_best_phases(&mut self, new_best: bool) -> usize {
         let mut alives: usize = 0;
         for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
             if let Some(b) = v.assign
                 && v.level > self.root_level
+                && !v.is(FlagVar::ELIMINATED)
             {
-                self.best_phases[vi] = (Some(b), v.level);
+                if new_best {
+                    self.best_phases[vi] = (Some(b), v.level);
+                }
                 alives += 1;
             } else {
-                self.best_phases[vi] = (None, DecisionLevel::MAX);
+                if new_best {
+                    self.best_phases[vi] = (None, DecisionLevel::MAX);
+                }
             }
         }
         self.num_vars - alives - self.num_asserted_vars - self.num_eliminated_vars
     }
+    fn clear_best_phases(&mut self) {
+        for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
+            if v.level > self.root_level && !v.is(FlagVar::ELIMINATED) {
+                self.best_phases[vi] = (None, DecisionLevel::MAX);
+            }
+        }
+    }
 }
 
 impl AssignStack {

src/assign/stack.rs

@@ -89,6 +89,9 @@ pub struct AssignStack {
     pub(super) activity_stay_rate: f64,
     /// its diff
     pub(super) activity_learning_rate: f64,
+
+    //## Misc
+    pub(super) rng: SplitMix64,
 }
 
 impl Default for AssignStack {
@@ -133,6 +136,7 @@ impl Default for AssignStack {
 
             activity_scheme: VarActivityScheme::default(),
             activity_learning_rate: 0.06,
+            rng: SplitMix64::new(0),
         }
     }
 }
@@ -171,6 +175,7 @@ impl Instantiate for AssignStack {
             activity_stay_rate: 1.0 - config.vrw_learning_rate,
 
             activity_learning_rate: config.vrw_learning_rate,
+            rng: SplitMix64::new((cnf.num_of_variables + cnf.num_of_clauses) as u64),
 
             ..AssignStack::default()
         }
@@ -199,6 +204,9 @@ impl AssignIF for AssignStack {
     fn root_level(&self) -> DecisionLevel {
         self.root_level
     }
+    fn current_conflict_index(&self) -> usize {
+        self.num_conflict
+    }
     fn stack(&self, i: usize) -> Lit {
         self.trail[i]
     }
@@ -382,7 +390,7 @@ impl fmt::Display for AssignStack {
                 f,
                 "ASG:: trail({}):[(0, {:?})]\n      level: {}, asserted: {}, eliminated: {}",
                 self.trail.len(),
-                &v,
+                v,
                 levels,
                 self.num_asserted_vars,
                 self.num_eliminated_vars,

src/bin/dmcr.rs

@@ -198,14 +198,14 @@ fn main() {
         None if from_file => println!(
             "{}A valid assignment set for {}{} is found in {}",
             green,
-            &args.problem.to_str().unwrap(),
+            args.problem.to_str().unwrap(),
             RESET,
-            &args.assign.unwrap().to_str().unwrap(),
+            args.assign.unwrap().to_str().unwrap(),
         ),
         None => println!(
             "{}A valid assignment set for {}.{}",
             green,
-            &args.problem.to_str().unwrap(),
+            args.problem.to_str().unwrap(),
             RESET,
         ),
     }