diff --git a/README.md b/README.md index fbfc31d16..9f036c748 100644 --- a/README.md +++ b/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 diff --git a/flake.lock b/flake.lock index 4e176efa1..bf0511ec2 100644 --- a/flake.lock +++ b/flake.lock @@ -181,11 +181,11 @@ }, "nixpkgs_11": { "locked": { - "lastModified": 1780002292, - "narHash": "sha256-O2k4sgDnoSSoZ5VgBfEwpso432pCpkLinkbTh7gswF4=", + "lastModified": 1781767213, + "narHash": "sha256-VeWB3PjXgFMU86hvpZXymfSAZv+T9+KgtEjaZGF1Ckk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "a840f3bfa7c71d222f07234bf357cb76c4cc6e57", + "rev": "746b8efb34046d34c265626788832b76b7699067", "type": "github" }, "original": { @@ -418,11 +418,11 @@ "nixpkgs": "nixpkgs_12" }, "locked": { - "lastModified": 1779920462, - "narHash": "sha256-c+h77EfDPZYplsRZKx2lJ+YtXg76iCQqiuOCgp5nfFs=", + "lastModified": 1781042363, + "narHash": "sha256-AwLy43zF8S1xUAWwOyuwPBOUSTEWOQ09y7yUPy2TjhA=", "owner": "shnarazk", "repo": "SAT-bench", - "rev": "c8b6217a2fe4472fb46531d94dd2e0cd37f4a519", + "rev": "8b750f2922dcc8228bd0fba23f4b0fb58f249599", "type": "github" }, "original": { diff --git a/src/assign/learning_rate.rs b/src/assign/learning_rate.rs index 5bc781daa..da757ea85 100644 --- a/src/assign/learning_rate.rs +++ b/src/assign/learning_rate.rs @@ -58,6 +58,10 @@ impl ActivityIF 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) { diff --git a/src/assign/mod.rs b/src/assign/mod.rs index 1258dd435..3889cc8b4 100644 --- a/src/assign/mod.rs +++ b/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. diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index deec2f027..d6d1a772a 100644 --- a/src/assign/propagate.rs +++ b/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 { diff --git a/src/assign/select.rs b/src/assign/select.rs index 27befb9f8..53c784d29 100644 --- a/src/assign/select.rs +++ b/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 { diff --git a/src/assign/stack.rs b/src/assign/stack.rs index 8855e0db5..a98e9e31b 100644 --- a/src/assign/stack.rs +++ b/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, diff --git a/src/bin/dmcr.rs b/src/bin/dmcr.rs index 2ec7add04..45556ce5d 100644 --- a/src/bin/dmcr.rs +++ b/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, ), } diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 3ae76c824..2934c155a 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -5,7 +5,7 @@ use { property, watch_cache::*, }, - crate::{assign::AssignIF, types::*}, + crate::{assign::AssignIF, state::State, types::*}, std::{ collections::HashMap, num::NonZeroU32, @@ -14,6 +14,7 @@ use { }, }; +use std::f64; #[cfg(not(feature = "no_IO"))] use std::{fs::File, io::Write, path::Path}; @@ -309,10 +310,6 @@ impl ClauseDBIF for ClauseDB { c.flags = FlagClause::empty(); debug_assert!(c.lits.is_empty()); // c.lits.clear(); std::mem::swap(&mut c.lits, vec); - c.search_from = 2; - c.referred_at = 0; - c.reference_rate = 1.0; - c.vivify_age = 0; } else { cid = ClauseId::from(self.clause.len()); let mut c = Clause { @@ -334,6 +331,11 @@ impl ClauseDBIF for ClauseDB { .. } = self; let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize]; + c.search_from = 2; + c.lbd = DecisionLevel::MAX; + c.vivify_age = 0; + c.vivify_at = 0; + c.reference_height = DecisionLevel::MAX; let len2 = c.lits.len() == 2; *num_clause += 1; if learnt { @@ -826,7 +828,15 @@ impl ClauseDBIF for ClauseDB { c.is(FlagClause::LEARNT) } /// reduce the number of 'learnt' or *removable* clauses. - fn reduce(&mut self, asg: &mut impl AssignIF, last_restart: usize) { + fn reduce(&mut self, asg: &impl AssignIF, state: &State) { + macro_rules! height { + ($c: expr) => { + $c.reference_height + $c.lbd + }; + } + let conflict_index: usize = asg.current_conflict_index(); + let effective_height: DecisionLevel = + (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel; self.num_reduction += 1; let ClauseDB { clause, @@ -842,9 +852,7 @@ impl ClauseDBIF for ClauseDB { } = self; *num_lbd2 = 0; let mut num_alives: usize = 0; - // tier 1 group: the small clauses under the best assignment let mut ntier1: usize = 0; - // tier 2 group: the small clauses under the best assignment let mut ntier2: usize = 0; for (i, c) in clause .iter_mut() @@ -853,41 +861,27 @@ impl ClauseDBIF for ClauseDB { .filter(|(_, c)| !c.is_dead()) { num_alives += 1; - match asg.literal_block_distance_current(&c.lits) { - 0..=2 => { - *num_lbd2 += 1; - continue; - } - 3 if c.reference_rate >= 0.01 => { - ntier1 += 1; - continue; - } - 4 if c.reference_rate >= 0.1 => { - ntier1 += 1; - continue; - } - 5 if c.reference_rate >= 2.0 => { - ntier2 += 1; - continue; - } - 6 if c.reference_rate >= 4.0 => { - ntier2 += 1; - continue; - } - 7 if c.reference_rate >= 8.0 => { - ntier2 += 1; - continue; - } - _ => {} - } - if c.len() <= 3 { - ntier1 += 1; + if !c.is(FlagClause::LEARNT) { + *num_lbd2 += (c.lbd <= 2) as usize; continue; } - if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) { + if c.is(FlagClause::ASSIGN_REASON) { + *num_lbd2 += (c.lbd <= 2) as usize; + // c.reference_height += 1.0; + // c.reference_height += c.lbd as f64; + // c.reference_height += (c.lbd as f64).log2(); continue; } - if c.reference_rate >= 16.0 || c.referred_at >= last_restart { + // Don't introduce any length-based crteria! + // Clause lengths without context make result worse. + if height!(c) <= effective_height + && (c.reference_height <= 4 || (conflict_index - c.referred_at) <= 800_000) + { + match c.lbd { + 0..=2 => *num_lbd2 += 1, + 3..=6 => ntier1 += 1, + _ => ntier2 += 1, + } continue; } remove_clause_fn( @@ -905,17 +899,17 @@ impl ClauseDBIF for ClauseDB { self.tier1_clauses.update(ntier1 as f64 / num_alives as f64); self.tier2_clauses.update(ntier2 as f64 / num_alives as f64); } - fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool) { - if clear { - for c in self.clause.iter_mut().skip(1) { - c.turn_off(FlagClause::BEST_PROPAGATOR); - } - } - for l in asg.stack_iter() { - if let AssignReason::Implication(cid) = asg.reason(l.vi()) { - self[cid].turn_on(FlagClause::BEST_PROPAGATOR); - } - } + fn save_best_assign_reasons(&mut self, _asg: &impl AssignIF, _clear: bool) { + // if clear { + // for c in self.clause.iter_mut().skip(1) { + // c.turn_off(FlagClause::BEST_PROPAGATOR); + // } + // } + // for l in asg.stack_iter() { + // if let AssignReason::Implication(cid) = asg.reason(l.vi()) { + // self[cid].turn_on(FlagClause::BEST_PROPAGATOR); + // } + // } } fn certificate_add_assertion(&mut self, lit: Lit) { self.certification_store.add_clause(&[lit]); diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 4cd850450..81116ffee 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -23,7 +23,7 @@ pub use self::{ }; use { - crate::{assign::AssignIF, types::*}, + crate::{assign::AssignIF, state::State, types::*}, std::{ ops::IndexMut, slice::{Iter, IterMut}, @@ -103,7 +103,7 @@ pub trait ClauseDBIF: /// reduce learnt clauses /// # CAVEAT /// *precondition*: decision level == 0. - fn reduce(&mut self, asg: &mut impl AssignIF, last_restart: usize); + fn reduce(&mut self, asg: &impl AssignIF, state: &State); /// turn `FlagClause::BEST_PROPAGATOR` of 'used clauses' on fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool); /// update flags. diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index 4db521806..05926995b 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -14,21 +14,22 @@ pub trait VivifyIF { impl VivifyIF for ClauseDB { /// vivify clauses under `asg` fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent { + // This is a reusable vector to reduce memory consumption, + // the key is the number of invocation + // let db_skip: usize = 1 + self.num_clause / 1_000_000; + let mut seen: Vec = vec![0; asg.num_vars + 1]; + let display_step: usize = 1000; + let mut num_check: usize = 0; + let mut num_shrink: usize = 0; + let mut num_assert: usize = 0; + let mut to_display: usize = display_step; + state[Stat::Vivification] += 1; if asg.remains() { asg.propagate_sandbox(self).map_err(|cc| { state.log(None, "By vivifier"); SolverError::RootLevelConflict(cc) })?; } - // This is a reusable vector to reduce memory consumption, - // the key is the number of invocation - let mut seen: Vec = vec![0; asg.num_vars + 1]; - let display_step: usize = 1000; - let mut num_check = 0; - let mut num_shrink = 0; - let mut num_assert = 0; - let mut to_display = 0; - state[Stat::Vivification] += 1; // Inlined target selection (formerly `select_targets`). // Pick clauses that haven't been vivified recently. We deliberately // do NOT sort the candidates: the per-clause filter in the loop below @@ -39,25 +40,27 @@ impl VivifyIF for ClauseDB { if c.is_dead() { continue; } - if c.referred_at + 20_000 * (1 + c.vivify_age) > asg.num_conflict || c.vivify_age >= 8 { + let span: usize = 10_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1); + if c.vivify_at + span > asg.num_conflict + || (c.referred_at <= c.vivify_at && (c.is(FlagClause::LEARNT) || c.vivify_age != 0)) + { continue; } + num_check += 1; let c = &mut self[cid]; - c.vivified(); + // c.update_reference_rate(asg.num_conflict); // Skip clauses that are unlikely to be improved by vivification. // Empirically success concentrates on clauses // that are not too short and have a moderate LBD; outside this band // the success rate collapses, so skipping them saves work without // losing many improvable clauses. - if c.len() < 9_usize.saturating_sub(c.vivify_age).max(3) - || 12 < asg.literal_block_distance_current(&c.lits) - { - continue; - } + // assert!(!c.is(FlagClause::ASSIGN_REASON)); + c.vivify_at = asg.num_conflict; + c.vivify_age += 1; let is_learnt = c.is(FlagClause::LEARNT); - let vivify_age = c.vivify_age; - let referred_at = c.referred_at; - let reference_rate = c.reference_rate; + let lbd = c.lbd; + let vivify_at = c.vivify_at; + let reference_height = c.reference_height; let clits = c.iter().copied().collect::>(); if to_display <= num_check { state.flush(""); @@ -66,7 +69,6 @@ impl VivifyIF for ClauseDB { )); to_display = num_check + display_step; } - num_check += 1; // debug_assert!(clits.iter().all(|l| !clits.contains(&!*l))); // Build a clean environment // debug_assert!(asg.stack_is_empty() || !asg.remains()); @@ -131,7 +133,6 @@ impl VivifyIF for ClauseDB { } match vec.len() { 0 => { - state.flush(""); state[Stat::VivifiedClause] += num_shrink; state[Stat::VivifiedVar] += num_assert; state.log(None, "RootLevelConflict By vivify"); @@ -145,9 +146,9 @@ impl VivifyIF for ClauseDB { _ => { if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new() { - self[cid].referred_at = referred_at; - self[cid].reference_rate = reference_rate; - self[cid].vivify_age = vivify_age; + self[cid].reference_height = reference_height; + self[cid].vivify_at = vivify_at; + self[cid].lbd = lbd.min(decisions.len() as DecisionLevel); } self.remove_clause(cid); num_shrink += 1; @@ -289,13 +290,3 @@ impl AssignStack { learnt } } - -impl Clause { - /// clear flags about vivification - fn vivified(&mut self) { - self.vivify_age += 1; - self.reference_rate *= 0.8; - self.reference_rate += 0.2 * self.referred as f64; - self.referred = 0; - } -} diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index 61bc87b4e..180018831 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -94,6 +94,9 @@ pub fn eliminate_var( RefClause::Clause(ci) => { // the merged clause might be a duplicated clause. elim.add_cid_occur(asg, ci, &mut cdb[ci], true); + cdb[ci].reference_height = + cdb[*p].reference_height.min(cdb[*n].reference_height); + cdb[ci].lbd = cdb[*p].lbd.max(cdb[*n].lbd); #[cfg(feature = "trace_elimination")] println!( diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index c29a91ba1..a7e04b5c2 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -134,12 +134,19 @@ pub fn handle_conflict( } } AssignReason::Implication(r) => { + let mut cs = Vec::new(); for l in cdb[r].iter() { let vi = l.vi(); if !bumped.contains(&vi) { asg.reward_at_analysis(vi); bumped.push(vi); } + if let AssignReason::Implication(ci) = asg.reason(l.vi()) { + cs.push((asg.level(l.vi()), ci)); + } + } + for (lvl, ci) in cs.into_iter() { + cdb[ci].reference_height = cdb[ci].reference_height.min(lvl); } } AssignReason::Decision(_) => (), @@ -216,7 +223,6 @@ pub fn handle_conflict( asg.assign_by_implication(l0, AssignReason::Implication(cid), assign_level); cdb[cid].turn_on(FlagClause::ASSIGN_REASON); } - cdb[cid].reference_rate = 1.0; // lbd should be calculated at conflict level, where all literals are assigned. // But since vars hold the last level even after unassignment, // we can have postponed the calculation. @@ -422,8 +428,10 @@ fn conflict_analyze( trace!(q, " -- ignore flagged already"); } } - cdb[cid].referred_at = asg.num_conflict; - cdb[cid].referred += 1; + cdb[cid].update_reference(asg); + cdb[cid].lbd = cdb[cid] + .lbd + .min(asg.literal_block_distance_current(&cdb[cid].lits)); } AssignReason::Decision(_) | AssignReason::None => {} } @@ -610,7 +618,7 @@ fn lit_level( cdb[cid].lit0(), lit, cid, - &cdb[cid] + cdb[cid] ); // assert!( // !bag.contains(&lit), diff --git a/src/solver/search.rs b/src/solver/search.rs index 0ef569efa..8e444f26a 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -224,13 +224,12 @@ impl SolveIF for Solver { } /// table of (RephaseTarget, span length, next index) -const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 6] = [ - (RephaseTarget::False, 20, 1), - (RephaseTarget::Walk, 60, 2), - (RephaseTarget::True, 20, 3), - (RephaseTarget::Best, 80, 4), - (RephaseTarget::Inverted, 20, 5), - (RephaseTarget::Walk, 60, 0), +const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 5] = [ + (RephaseTarget::Polarity, 8, 1), + (RephaseTarget::False, 2, 2), + (RephaseTarget::True, 2, 3), + (RephaseTarget::Best, 2, 4), + (RephaseTarget::Walk, 8, 0), ]; /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT. @@ -240,18 +239,19 @@ fn search( state: &mut State, ) -> Result { let mut span_len: usize = 1; - let mut vivificatioen_pressure: usize = 0; - let vivificatioen_interval: usize = 8_000; let mut elimination_pressure: usize = 0; let elimination_interval: usize = 80_000; let mut progress_pressure: usize = 0; let progress_interval: usize = 10_000; let mut reduction_pressure: usize = 0; + let reduction_interval: usize = 80_000; let mut rephase_rotation_pressure: usize = 0; + let mut vivification_pressure: usize = 0; + let vivification_interval: usize = 20_000; let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0]; let vmtf_interval: usize = 20; let mut assign_peak: usize = 0; - let luby_scale: usize = 64; + let luby_scale: usize = 32; let mut span_scale: usize = luby_scale; macro_rules! reduce { @@ -259,14 +259,16 @@ fn search( state.search_mode_ratio.0.update(0.0); state.search_mode_ratio.1.update(0.0); reduction_pressure = 0; - cdb.reduce(asg, state.last_restart) + cdb.reduce(asg, state); }}; } macro_rules! to_lrb { () => { if asg.activity_scheme != VarActivityScheme::LRB { asg.activity_scheme = VarActivityScheme::LRB; - asg.set_learning_rate(state.config.vrw_learning_rate); + let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64; + let adaptive_lr: f64 = 1.0 / span.sqrt(); + asg.set_learning_rate(adaptive_lr); asg.rebuild_order(); } current_phase = &REPHASE_ROTATION[0]; @@ -278,8 +280,7 @@ fn search( () => { if asg.activity_scheme != VarActivityScheme::VMTF { asg.activity_scheme = VarActivityScheme::VMTF; - // asg.phase_mode = RephaseTarget::Walk; - // asg.phase_mode = RephaseTarget::Best; + asg.phase_mode = RephaseTarget::Walk; asg.set_learning_rate(0.0); // Don't change this asg.rebuild_order(); rephase_rotation_pressure = 0; @@ -292,7 +293,13 @@ fn search( asg.phase_mode = current_phase.0; rephase_rotation_pressure = 0; // if current_phase.2 == 0 { - // to_vmtf!(); + // current_phase = &REPHASE_ROTATION[current_phase.2]; + // asg.phase_mode = current_phase.0; + // rephase_rotation_pressure = 0; + // // asg.clear_best_phases(); + // // state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar); + // // assign_peak = 0; + // // to_vmtf!(); // } else { // current_phase = &REPHASE_ROTATION[current_phase.2]; // asg.phase_mode = current_phase.0; @@ -306,6 +313,7 @@ fn search( if let Some(core) = asg.check_best_phases() { assign_peak = assign_peak.saturating_sub(2 * $n); state.core_size = core; + to_vmtf!(); } else { assign_peak = 0; let pre = state.core_size; @@ -332,6 +340,7 @@ fn search( return Err(SolverError::RootLevelConflict(cc)); } asg.update_activity_tick(); + let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar); let (cid, lbd) = handle_conflict(asg, cdb, state, &cc)?; if cid == ClauseId::default() { match asg.activity_scheme { @@ -347,42 +356,62 @@ fn search( update_core!(1); } else { cdb.lbd.update(lbd as f64); + cdb[cid].lbd = DecisionLevel::MAX; } match asg.stack_len().cmp(&assign_peak) { Ordering::Less => {} Ordering::Equal => { - // Do not update best_phases here to avoid an oscilation + // Do not update best_phases as new_best here to avoid an oscilation + state.core_size = asg.save_best_phases(false); cdb.save_best_assign_reasons(asg, false); } Ordering::Greater => { assign_peak = asg.stack_len(); - state.core_size = asg.save_best_phases(); + state.core_size = asg.save_best_phases(true); cdb.save_best_assign_reasons(asg, false); state.flush(""); state.flush(format!("core: {}", state.core_size)); + // if state.core_size < 10 { + // for (i, v) in asg.var_iter().enumerate().skip(1) { + // if !v.is(FlagVar::ELIMINATED) && v.level > 0 { + // println!( + // "{:>4}: {:>2}| {:>6.3}", + // i, + // match v.assign { + // None => 0, + // Some(false) => -1, + // Some(true) => 1, + // }, + // v.polarity + // ); + // } + // } + // } } } elimination_pressure += 1; - vivificatioen_pressure += 1; progress_pressure += 1; reduction_pressure += 1; rephase_rotation_pressure += 1; + vivification_pressure += 1; span_len += 1; - if reduction_pressure >= 40_000 { + // Don't check with `>= 1 * reduction_interval`. It prevents `reduce!(true)`. + if reduction_pressure > reduction_interval { reduce!(); } if state.span_manager.span_ended(span_len / span_scale) { span_len = 0; let new_segment = state.span_manager.prepare_new_span(span_len); dump_stage(asg, state, new_segment); - let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar); RESTART!(asg, cdb, state)?; - if vivificatioen_pressure >= vivificatioen_interval { - if cfg!(feature = "clause_vivification") && current_phase.0 == RephaseTarget::Walk { - reduce!(); + // if reduction_pressure > reduction_interval { + // reduce!(); + // } + if vivification_pressure >= vivification_interval { + if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; } - vivificatioen_pressure = 0; + vivification_pressure = 0; } if elimination_pressure >= elimination_interval { if cfg!(feature = "clause_elimination") { @@ -393,11 +422,6 @@ fn search( } elimination_pressure = 0; } - let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar); - if unasserted_now != unasserted_pre { - update_core!(unasserted_pre - unasserted_now); - // to_vmtf!(); - } if cfg!(feature = "rephase") { match asg.activity_scheme { VarActivityScheme::LRB @@ -413,7 +437,7 @@ fn search( _ => (), } } - if new_segment == Some(true) { + if new_segment.is_some() { span_scale = luby_scale * state.span_manager.envelop_index(); // Adapt LRB learning rate to the upcoming Luby envelope height: // shorter spans → higher α (fast learning before the next restart), @@ -421,8 +445,16 @@ fn search( let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64; let adaptive_lr: f64 = 1.0 / span.sqrt(); asg.set_learning_rate(adaptive_lr); + } else { + asg.rescale_learning_rate(0.9); } } + let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar); + if unasserted_now != unasserted_pre { + state.last_assertion = asg.num_conflict; + update_core!(unasserted_pre - unasserted_now); + // to_vmtf!(); + } if progress_pressure >= progress_interval { state.progress(asg, cdb); if let Some(p) = state.elapsed() { diff --git a/src/state.rs b/src/state.rs index ac9053f5c..4be79afaa 100644 --- a/src/state.rs +++ b/src/state.rs @@ -123,6 +123,8 @@ pub struct State { pub core_size: usize, /// the last restart in conflicts pub last_restart: usize, + /// the last assertion in conflicts + pub last_assertion: usize, #[cfg(feature = "chrono_BT")] /// chronoBT threshold @@ -162,11 +164,12 @@ impl Default for State { Ema2::default().with_value(0.5), Ema2::default().with_value(0.5), ), - b_lvl: Ema2::default_extended(), - c_lvl: Ema2::default_extended(), + b_lvl: Ema2::default_extended().with_slow(80_000), + c_lvl: Ema2::default_extended().with_slow(80_000), bt_drift_average: Ema::default().with_span(1000), core_size: 0, last_restart: 0, + last_assertion: 0, #[cfg(feature = "chrono_BT")] chrono_bt_threshold: 100, @@ -875,7 +878,7 @@ impl fmt::Display for State { if width < vclen + fnlen + 1 { write!(f, "{fname:9.2}") } else { - write!(f, "{fname}{:>w$} |time:{tm:>9.2}", &vc, w = width - fnlen,) + write!(f, "{fname}{:>w$} |time:{tm:>9.2}", vc, w = width - fnlen,) } } } diff --git a/src/types/clause.rs b/src/types/clause.rs index bc8fe5d63..194cb8da3 100644 --- a/src/types/clause.rs +++ b/src/types/clause.rs @@ -17,14 +17,16 @@ pub struct Clause { /// the index from which `propagate` starts searching an un-falsified literal. /// Since it's just a hint, we don't need u32 or usize. pub search_from: u16, - /// Sum of activated (used as propagated) duration + /// The last reference time in conflict analysis pub(crate) referred_at: usize, - /// The average number of references in a vivification interval - pub(crate) reference_rate: f64, + /// The minimal decision level at which a conflict occured by this clause + pub(crate) reference_height: DecisionLevel, /// last vivified time in conflicts pub(crate) vivify_age: usize, - /// The number of referrences in conflict analysis - pub(crate) referred: usize, + // last vivified time in conflict + pub(crate) vivify_at: usize, + /// the minimal lbd of this clause so far + pub(crate) lbd: DecisionLevel, } /// API for Clause, providing literal accessors. @@ -47,6 +49,8 @@ pub trait ClauseIF { fn len(&self) -> usize; /// return true is this is a unit clause under `asg`. fn is_unit_under(&self, asg: &impl AssignIF) -> bool; + /// update reference_distance. + fn update_reference(&mut self, asg: &impl AssignIF); } impl Default for Clause { @@ -56,9 +60,10 @@ impl Default for Clause { flags: FlagClause::empty(), search_from: 2, referred_at: 0, - reference_rate: 1.0, + reference_height: DecisionLevel::MAX, vivify_age: 0, - referred: 0, + vivify_at: 0, + lbd: DecisionLevel::MAX, } } } @@ -215,6 +220,11 @@ impl ClauseIF for Clause { .all(|l| asg.assigned(*l) == Some(false)); unassigned == 1 && all_others_false } + fn update_reference(&mut self, asg: &impl AssignIF) { + self.referred_at = asg.current_conflict_index(); + let level = asg.decision_level(); + self.reference_height = self.reference_height.min(level); + } } impl FlagIF for Clause { diff --git a/src/types/flags.rs b/src/types/flags.rs index 816675d88..dffb36a45 100644 --- a/src/types/flags.rs +++ b/src/types/flags.rs @@ -25,8 +25,8 @@ bitflags! { const OCCUR_LINKED = 0b0000_0100; /// a clause is registered in vars' assing list. const ASSIGN_REASON = 0b0000_1000; - /// used in the best assignments - const BEST_PROPAGATOR = 0b0010_0000; + // /// used in the best assignments + // const BEST_PROPAGATOR = 0b0010_0000; } } @@ -35,18 +35,18 @@ bitflags! { #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] pub struct FlagVar: u8 { /// * the previous assigned value of a Var. - const PHASE = 0b0000_0001; + const PHASE = 0b0000_0001; /// used in conflict analyze - const USED = 0b0000_0010; + const USED = 0b0000_0010; /// a var is eliminated and managed by eliminator. - const ELIMINATED = 0b0000_0100; + const ELIMINATED = 0b0000_0100; /// a clause or var is enqueued for eliminator. - const ENQUEUED = 0b0000_1000; + const ENQUEUED = 0b0000_1000; /// a var is checked during in the current conflict analysis. - const CA_SEEN = 0b0001_0000; + const CA_SEEN = 0b0001_0000; #[cfg(feature = "trace_propagation")] /// check propagation - const PROPAGATED = 0b0010_0000; + const PROPAGATED = 0b0010_0000; } } diff --git a/src/types/mod.rs b/src/types/mod.rs index 0b55adc61..13a17ca93 100644 --- a/src/types/mod.rs +++ b/src/types/mod.rs @@ -15,12 +15,16 @@ pub mod idx; pub mod lit; /// methods on binary link, namely binary clause pub mod luby; +/// a deterministic pseudo-random number generator +pub mod rng; /// methods on f64 sort pub mod sort_key; /// methods on Var pub mod var; -pub use self::{clause::*, cnf::*, ema::*, flags::*, idx::*, lit::*, luby::*, sort_key::*, var::*}; +pub use self::{ + clause::*, cnf::*, ema::*, flags::*, idx::*, lit::*, luby::*, rng::*, sort_key::*, var::*, +}; pub use crate::{assign::AssignReason, config::Config, solver::SolverEvent}; @@ -58,6 +62,7 @@ pub trait ActivityIF { fn set_learning_rate(&mut self, learning_rate: f64); /// update internal counter. fn update_activity_tick(&mut self); + fn rescale_learning_rate(&mut self, scaling: f64); } /// API for object instantiation based on `Configuration` and `CNFDescription`. diff --git a/src/types/rng.rs b/src/types/rng.rs new file mode 100644 index 000000000..b0f2e5870 --- /dev/null +++ b/src/types/rng.rs @@ -0,0 +1,91 @@ +//! A deterministic, dependency-free pseudo-random number generator. +//! +//! The standard library does not provide a general-purpose RNG, so this is a +//! small [SplitMix64](https://prng.di.unimi.it/splitmix64.c) generator. It is +//! fully deterministic (the same seed always yields the same sequence), fast, +//! and of high statistical quality, which makes it suitable for reproducible +//! randomization inside the solver. + +/// A SplitMix64 pseudo-random number generator. +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub struct SplitMix64 { + state: u64, +} + +impl Default for SplitMix64 { + fn default() -> Self { + SplitMix64::new(0) + } +} + +impl SplitMix64 { + /// Create a generator from a seed. Any seed (including `0`) is valid. + pub const fn new(seed: u64) -> Self { + SplitMix64 { state: seed } + } + /// Return the next 64-bit pseudo-random value and advance the state. + pub fn next_u64(&mut self) -> u64 { + self.state = self.state.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.state; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + /// Return a pseudo-random `f64` in the half-open range `[0.0, 1.0)`. + pub fn next_f64(&mut self) -> f64 { + // Use the top 53 bits to fill the mantissa of an f64. + (self.next_u64() >> 11) as f64 / ((1u64 << 53) as f64) + } + /// Return a pseudo-random `bool`. + pub fn next_bool(&mut self) -> bool { + self.next_u64().is_multiple_of(2) + } + /// Return a pseudo-random `usize` in the half-open range `[0, bound)`. + /// Returns `0` when `bound` is `0`. + pub fn below(&mut self, bound: usize) -> usize { + if bound == 0 { + 0 + } else { + (self.next_u64() % bound as u64) as usize + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_deterministic() { + let mut a = SplitMix64::new(12345); + let mut b = SplitMix64::new(12345); + for _ in 0..1000 { + assert_eq!(a.next_u64(), b.next_u64()); + } + } + + #[test] + fn test_distinct_seeds_diverge() { + let mut a = SplitMix64::new(1); + let mut b = SplitMix64::new(2); + assert_ne!(a.next_u64(), b.next_u64()); + } + + #[test] + fn test_next_f64_in_range() { + let mut r = SplitMix64::new(42); + for _ in 0..10_000 { + let x = r.next_f64(); + assert!((0.0..1.0).contains(&x)); + } + } + + #[test] + fn test_below_bound() { + let mut r = SplitMix64::new(7); + for _ in 0..10_000 { + assert!(r.below(10) < 10); + } + assert_eq!(r.below(0), 0); + } +} diff --git a/src/types/var.rs b/src/types/var.rs index fe79cd3bf..39b865abd 100644 --- a/src/types/var.rs +++ b/src/types/var.rs @@ -25,6 +25,11 @@ pub struct Var { pub(crate) reward: f64, /// the last conflict by this pub(crate) last_conflict: usize, + /// phase bias at the best assignments + /// - 1.0: `true` always + /// - 0.0: no bias + /// - -1.0: `false` always + pub(crate) polarity: f64, } impl Default for Var { @@ -38,6 +43,7 @@ impl Default for Var { flags: FlagVar::empty(), reward: 0.0, last_conflict: 0, + polarity: 0.0, } } }