From 5ebd4233f71d3bf8abc464590bd57e65e9cf254c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 22 Sep 2024 03:02:25 +0900 Subject: [PATCH 01/27] Initialize Clause::{rank|rank_old} correctly --- Cargo.lock | 4 ++-- src/cdb/clause.rs | 11 +++++++---- src/cdb/mod.rs | 6 ++++-- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ec623dd7f..57ec2655c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -528,9 +528,9 @@ dependencies = [ [[package]] name = "unicode-width" -version = "0.1.13" +version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d" +checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" [[package]] name = "version_check" diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs index b55326816..cbeb0a768 100644 --- a/src/cdb/clause.rs +++ b/src/cdb/clause.rs @@ -100,8 +100,8 @@ impl Default for Clause { ], lits: vec![Lit::default(), Lit::default()], flags: FlagClause::empty(), - rank: 0, - rank_old: 0, + rank: u32::MAX, + rank_old: u32::MAX, search_from: 2, #[cfg(any(feature = "boundary_check", feature = "clause_rewarding"))] @@ -327,7 +327,10 @@ impl Clause { cnt += 1; } } - self.rank = cnt; - cnt + if cnt < self.rank { + self.rank_old = self.rank; + self.rank = cnt; + } + self.rank } } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 2d15505aa..139ca518c 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -270,7 +270,6 @@ impl ClauseDBIF for ClauseDB { debug_assert_eq!(l1, self[ci].lits[1]); } self.clause[ci].search_from = 0; - self.clause[ci].rank_old = self[ci].rank; self.lbd.update(self[ci].rank); self.num_clause += 1; if learnt { @@ -1157,7 +1156,10 @@ impl ClauseWeaverIF for ClauseDB { ); debug_assert_ne!(next, self.watch[FREE_LIT].next); debug_assert_ne!(0, next.as_ci()); - next.as_ci() + let ci = next.as_ci(); + self.clause[ci].rank = u32::MAX; + self.clause[ci].rank_old = u32::MAX; + ci } } // Check whether a zombi exists From 50603c10a3e35e7eb18eea79765c9e3f5994068e Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 22 Sep 2024 03:04:11 +0900 Subject: [PATCH 02/27] Add StageManager::segment_progress_ratio --- src/cdb/ema.rs | 4 ++-- src/primitive/ema.rs | 12 ------------ src/solver/stage.rs | 19 ++++++++++++------- src/state.rs | 6 +++++- 4 files changed, 19 insertions(+), 22 deletions(-) diff --git a/src/cdb/ema.rs b/src/cdb/ema.rs index a2b031d78..abaed3470 100644 --- a/src/cdb/ema.rs +++ b/src/cdb/ema.rs @@ -14,7 +14,7 @@ pub struct ProgressLBD { impl Default for ProgressLBD { fn default() -> ProgressLBD { ProgressLBD { - ema: Ewa2::new(0.0).with_value(16.0), + ema: Ewa2::new(0.0), num: 0, sum: 0, } @@ -24,7 +24,7 @@ impl Default for ProgressLBD { impl Instantiate for ProgressLBD { fn instantiate(_config: &Config, _: &CNFDescription) -> Self { ProgressLBD { - ema: Ewa2::new(0.0).with_slow(LBD_EWA_SLOW).with_value(16.0), + ema: Ewa2::new(0.0).with_slow(LBD_EWA_SLOW), ..ProgressLBD::default() } } diff --git a/src/primitive/ema.rs b/src/primitive/ema.rs index 056a3b7b4..f5a7c9eb4 100644 --- a/src/primitive/ema.rs +++ b/src/primitive/ema.rs @@ -17,13 +17,6 @@ pub trait EmaIF { } } -pub trait EmaSingleIF: EmaIF { - /// return the current value. - fn get(&self) -> f64 { - self.get_fast() - } -} - /// API for Exponential Moving Average, EMA, like `get`, `reset`, `update` and so on. pub trait EmaMutIF: EmaIF { /// the type of the argument of `update`. @@ -437,9 +430,4 @@ impl Ewa2 { self.sx = 1.0 - self.se; self } - pub fn with_value(mut self, val: f64) -> Self { - self.ema.fast = val; - self.ema.slow = val; - self - } } diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 165c16ead..e156d94b0 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -152,13 +152,6 @@ impl StageManager { pub fn current_segment(&self) -> usize { self.segment } - /// returns a recommending number of redicible learnt clauses, based on - /// the length of span. - pub fn num_reducible(&self, reducing_factor: f64) -> usize { - let span: f64 = self.span_ema.get(); - let keep = span.powf(1.0 - reducing_factor) as usize; - (span as usize).saturating_sub(keep) - } /// returns the maximum factor so far. /// None: `luby_iter.max_value` holds the maximum value so far. /// This means it is the value found at the last segment. @@ -166,6 +159,11 @@ impl StageManager { pub fn max_scale(&self) -> usize { self.max_scale_of_segment } + /// returns (0, 1] + pub fn segment_progress_ratio(&self) -> f64 { + (2 * (self.cycle - self.segment_starting_cycle + 1)) as f64 + / self.max_scale_of_segment as f64 + } pub fn cycle_starting_stage(&self) -> usize { self.cycle_starting_stage } @@ -181,4 +179,11 @@ impl StageManager { pub fn set_span_base(&mut self, span_base: f64) { self.span_base = span_base; } + /// returns a recommending number of redicible learnt clauses, based on + /// the length of span. + pub fn num_reducible(&self, reducing_factor: f64) -> usize { + let span: f64 = self.span_ema.get(); + let keep = span.powf(1.0 - reducing_factor) as usize; + (span as usize).saturating_sub(keep) + } } diff --git a/src/state.rs b/src/state.rs index 4e7753afc..456985d34 100644 --- a/src/state.rs +++ b/src/state.rs @@ -559,7 +559,11 @@ impl StateIF for State { println!( // "\x1B[2K misc|ccut:{}, vdcy:{}, core:{}, /ppc:{}", "\x1B[2K{:>12}|ccut:{}, vdcy:{}, core:{}, /ppc:{}", - format!("Luby{}", self.stm.current_segment(),), + format!( + "Luby{},{:>4.2}", + self.stm.current_segment(), + self.stm.segment_progress_ratio(), + ), fm!( "{:>9.4}", self, From 8525b77b904b42fb108a0d7bf7f9f7432669a8df Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 22 Sep 2024 03:05:40 +0900 Subject: [PATCH 03/27] Skip LBD calculation if clauses are good enough --- src/cdb/mod.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 139ca518c..f2472dec9 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -575,6 +575,9 @@ impl ClauseDBIF for ClauseDB { ref mut lbd_temp, .. } = self; + if clause[ci].rank < threshold as DecisionLevel { + continue; + } clause[ci].update_lbd(asg, lbd_temp); if threshold < clause[ci].extended_lbd() { // keep -= 1; From ad2e7af261a6c2f46793bdaea26f8bbf051a965c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 07:04:10 +0900 Subject: [PATCH 04/27] Remove Ewa, Implement some missing functions --- src/assign/ema.rs | 10 +++++----- src/cdb/ema.rs | 10 +++++----- src/primitive/ema.rs | 10 ++++++++++ 3 files changed, 20 insertions(+), 10 deletions(-) diff --git a/src/assign/ema.rs b/src/assign/ema.rs index dbaf90f59..545a2b596 100644 --- a/src/assign/ema.rs +++ b/src/assign/ema.rs @@ -1,18 +1,18 @@ use crate::types::*; -const ASG_EWA_LEN: usize = 16; -const ASG_EWA_SLOW: usize = 8192; +const ASG_EMA_LEN: usize = 16; +const ASG_EMA_SLOW: usize = 8192; /// An assignment history used for blocking restart. #[derive(Clone, Debug)] pub struct ProgressASG { - ema: Ewa2, + ema: Ema2, } impl Default for ProgressASG { fn default() -> ProgressASG { ProgressASG { - ema: Ewa2::::new(0.0), + ema: Ema2::new(ASG_EMA_LEN).with_slow(ASG_EMA_SLOW), } } } @@ -20,7 +20,7 @@ impl Default for ProgressASG { impl Instantiate for ProgressASG { fn instantiate(_config: &Config, _cnf: &CNFDescription) -> Self { ProgressASG { - ema: Ewa2::new(0.0).with_slow(ASG_EWA_SLOW), + ema: Ema2::new(ASG_EMA_LEN).with_slow(ASG_EMA_SLOW), } } } diff --git a/src/cdb/ema.rs b/src/cdb/ema.rs index abaed3470..f1622f1aa 100644 --- a/src/cdb/ema.rs +++ b/src/cdb/ema.rs @@ -1,12 +1,12 @@ use crate::types::*; -const LBD_EWA_LEN: usize = 16; -const LBD_EWA_SLOW: usize = 8192; +const LBD_EMA_LEN: usize = 16; +const LBD_EMA_SLOW: usize = 8192; /// An EMA of learnt clauses' LBD, used for forcing restart. #[derive(Clone, Debug)] pub struct ProgressLBD { - ema: Ewa2, + ema: Ema2, num: usize, sum: usize, } @@ -14,7 +14,7 @@ pub struct ProgressLBD { impl Default for ProgressLBD { fn default() -> ProgressLBD { ProgressLBD { - ema: Ewa2::new(0.0), + ema: Ema2::new(LBD_EMA_LEN).with_slow(LBD_EMA_SLOW), num: 0, sum: 0, } @@ -24,7 +24,7 @@ impl Default for ProgressLBD { impl Instantiate for ProgressLBD { fn instantiate(_config: &Config, _: &CNFDescription) -> Self { ProgressLBD { - ema: Ewa2::new(0.0).with_slow(LBD_EWA_SLOW), + ema: Ema2::new(LBD_EMA_LEN).with_slow(LBD_EMA_SLOW), ..ProgressLBD::default() } } diff --git a/src/primitive/ema.rs b/src/primitive/ema.rs index f5a7c9eb4..433a76f06 100644 --- a/src/primitive/ema.rs +++ b/src/primitive/ema.rs @@ -89,6 +89,12 @@ impl EmaIF for Ema { } impl EmaMutIF for Ema { + fn reset_to(&mut self, val: f64) { + self.val.fast = val; + } + fn reset_fast(&mut self) { + self.val.fast = 0.0; + } type Input = f64; #[cfg(not(feature = "EMA_calibration"))] fn update(&mut self, x: Self::Input) { @@ -197,6 +203,7 @@ impl EmaMutIF for Ema2 { } fn reset_to(&mut self, val: f64) { self.ema.fast = val; + self.ema.slow = val; } #[cfg(not(feature = "EMA_calibration"))] fn reset_fast(&mut self) { @@ -303,6 +310,7 @@ impl EmaSU { } } +/* /// Equally-Weighted-Average, namely, Average #[derive(Clone, Debug)] pub struct Ewa { @@ -386,6 +394,7 @@ impl EmaMutIF for Ewa2 { } fn reset_to(&mut self, val: f64) { self.ema.fast = val; + self.ema.slow = val; } #[cfg(not(feature = "EMA_calibration"))] fn reset_fast(&mut self) { @@ -431,3 +440,4 @@ impl Ewa2 { self } } +*/ From db48677f44890e4928f97e754bb77d7fa1f95e36 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 18:43:16 +0900 Subject: [PATCH 05/27] Vivify does not change caluse's flags --- src/cdb/vivify.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index 5a5ae9270..cf7f04f59 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -102,8 +102,8 @@ impl VivifyIF for ClauseDB { } AssignReason::Implication(wli) => { if wli.as_ci() == ci && clits.len() == decisions.len() { - #[cfg(feature = "keep_just_used_clauses")] - self.clause[wli.as_ci()].turn_on(FlagClause::USED); + // #[cfg(feature = "keep_just_used_clauses")] + // self.clause[ci].turn_on(FlagClause::??); asg.backtrack_sandbox(); continue 'next_clause; } else { @@ -280,8 +280,8 @@ impl AssignStack { seen[bil.vi()] = key; } AssignReason::Implication(wli) => { - #[cfg(feature = "keep_just_used_clauses")] - cdb.clause[wli.as_ci()].turn_on(FlagClause::USED); + // #[cfg(feature = "keep_just_used_clauses")] + // cdb.clause[wli.as_ci()].turn_on(FlagClause::USED); for (i, r) in cdb[wli.as_ci()].iter().enumerate() { if i == wli.as_wi() { continue; From e4647b16d0285046bde5767a83c9401698ff6aed Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 18:48:19 +0900 Subject: [PATCH 06/27] Add `{AssignStack|State}.clause_generation_shift` --- src/assign/stack.rs | 2 ++ src/state.rs | 7 +++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/assign/stack.rs b/src/assign/stack.rs index 9fe88b5b9..8330dbf48 100644 --- a/src/assign/stack.rs +++ b/src/assign/stack.rs @@ -47,6 +47,7 @@ pub struct AssignStack { // //## Stage // + pub clause_generation_shift: Ema, pub stage_scale: usize, //## Elimanated vars @@ -125,6 +126,7 @@ impl Default for AssignStack { #[cfg(feature = "rephase")] phase_age: 0, + clause_generation_shift: Ema::new(12000), stage_scale: 1, eliminated: Vec::new(), diff --git a/src/state.rs b/src/state.rs index 456985d34..7cba85621 100644 --- a/src/state.rs +++ b/src/state.rs @@ -112,6 +112,8 @@ pub struct State { /// chrono_BT threshold pub chrono_bt_threshold: DecisionLevel, + /// for clause reduction + pub clause_generation_shift: Ema, /// hold the previous number of non-conflicting assignment pub last_asg: usize, /// working place to build learnt clauses @@ -157,6 +159,7 @@ impl Default for State { #[cfg(feature = "chrono_BT")] chrono_bt_threshold: 100, + clause_generation_shift: Ema::new(12000), last_asg: 0, new_learnt: Vec::new(), derive20: Vec::new(), @@ -560,9 +563,9 @@ impl StateIF for State { // "\x1B[2K misc|ccut:{}, vdcy:{}, core:{}, /ppc:{}", "\x1B[2K{:>12}|ccut:{}, vdcy:{}, core:{}, /ppc:{}", format!( - "Luby{},{:>4.2}", + "Luby{}.{:0>2}", self.stm.current_segment(), - self.stm.segment_progress_ratio(), + ((self.stm.segment_progress_ratio() * 100.0) as usize - 1).clamp(0, 99), ), fm!( "{:>9.4}", From c3e0b27f5004528251a3810d993fb9219899ef6e Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 18:50:36 +0900 Subject: [PATCH 07/27] Add/rename `FlagClause::{NEW_CLAUSE|FORWD_LINK|BCKWD_LINK}` --- src/assign/propagate.rs | 8 +++++++- src/cdb/mod.rs | 8 ++++---- src/processor/eliminate.rs | 9 +++++++++ src/solver/conflict.rs | 5 ++++- src/types.rs | 16 ++++++++++------ 5 files changed, 34 insertions(+), 12 deletions(-) diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index c0d7a1d3e..ff5d3510d 100644 --- a/src/assign/propagate.rs +++ b/src/assign/propagate.rs @@ -376,7 +376,13 @@ impl PropagateIF for AssignStack { debug_assert_eq!(self.assigned(other), None); #[cfg(feature = "keep_just_used_clauses")] - c.turn_on(FlagClause::USED); + { + if !c.is(FlagClause::FORWD_LINK) { + let b = c.is(FlagClause::NEW_CLAUSE); + self.clause_generation_shift.update(b as u8 as f64); + } + c.turn_on(FlagClause::FORWD_LINK); + } self.assign_by_implication( other, if len == 0 { diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index f2472dec9..50975145e 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -291,7 +291,7 @@ impl ClauseDBIF for ClauseDB { } #[cfg(feature = "keep_just_used_clauses")] { - self.clause[ci].turn_on(FlagClause::USED); + self.clause[ci].turn_on(FlagClause::NEW_CLAUSE); } // assert_ne!(self.clause[ci].lit0(), self.clause[ci].lit1()); RefClause::Clause(ci) @@ -518,7 +518,7 @@ impl ClauseDBIF for ClauseDB { let learnt = c.is(FlagClause::LEARNT); if learnt { #[cfg(feature = "keep_just_used_clauses")] - c.turn_on(FlagClause::USED); + c.turn_on(FlagClause::NEW_CLAUSE); #[cfg(feature = "clause_rewarding")] self.reward_at_analysis(ci); } @@ -1387,7 +1387,7 @@ mod tests { assert!(!c.is_dead()); assert!(!c.is(FlagClause::LEARNT)); #[cfg(feature = "keep_just_used_clauses")] - assert!(c.is(FlagClause::USED)); + assert!(c.is(FlagClause::NEW_CLAUSE)); let c2 = cdb .new_clause(&mut asg, &mut vec![lit(-1), lit(2), lit(3)], true) .as_ci(); @@ -1395,7 +1395,7 @@ mod tests { assert!(!c.is_dead()); assert!(c.is(FlagClause::LEARNT)); #[cfg(feature = "keep_just_used_clauses")] - assert!(c.is(FlagClause::USED)); + assert!(c.is(FlagClause::NEW_CLAUSE)); } #[test] fn test_clause_equality() { diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index 4766834e1..7117c7b43 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -94,6 +94,15 @@ pub fn eliminate_var( // the merged clause might be a duplicated clause. elim.add_cid_occur(asg, ci, &mut cdb[ci], true); + for flg in [ + FlagClause::NEW_CLAUSE, + FlagClause::FORWD_LINK, + FlagClause::BCKWD_LINK, + ] { + let val: bool = cdb[*p].is(flg) || cdb[*n].is(flg); + cdb[ci].set(flg, val); + } + #[cfg(feature = "trace_elimination")] println!( " - eliminate_var {}: X {} from {} and {}", diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index d7072d846..db43f67be 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -353,8 +353,11 @@ fn conflict_analyze( state.derive20.push(ci); } else { #[cfg(feature = "keep_just_used_clauses")] - cdb[ci].turn_on(FlagClause::USED); + cdb[ci].turn_on(FlagClause::FORWD_LINK); } + state + .clause_generation_shift + .update(cdb[ci].is(FlagClause::FORWD_LINK) as u8 as f64); if max_lbd < cdb[ci].rank { max_lbd = cdb[ci].rank; ci_with_max_lbd = Some(ci); diff --git a/src/types.rs b/src/types.rs index 07e161c3c..f35d1af29 100644 --- a/src/types.rs +++ b/src/types.rs @@ -558,18 +558,22 @@ pub trait FlagIF { bitflags! { /// Misc flags used by [`Clause`](`crate::cdb::Clause`). - #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] + #[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] pub struct FlagClause: u8 { /// a clause is a generated clause by conflict analysis and is removable. const LEARNT = 0b0000_0001; - /// used in conflict analyze - const USED = 0b0000_0010; + /// used as unit propagation + const NEW_CLAUSE = 0b0000_0010; + /// used as unit propagation + const FORWD_LINK = 0b0000_0100; + /// used in conflict analysis + const BCKWD_LINK = 0b0000_1000; /// a clause or var is enqueued for eliminator. - const ENQUEUED = 0b0000_0100; + const ENQUEUED = 0b0001_0000; /// a clause is registered in vars' occurrence list. - const OCCUR_LINKED = 0b0000_1000; + const OCCUR_LINKED = 0b0010_0000; /// a given clause derived a learnt which LBD is smaller than 20. - const DERIVE20 = 0b0001_0000; + const DERIVE20 = 0b0100_0000; } } From cc635277ab67def317de2810e5ed5126755693c5 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 18:52:50 +0900 Subject: [PATCH 08/27] Use them --- src/cdb/mod.rs | 25 +++++++++++++++++++++++-- src/solver/conflict.rs | 15 ++++++++++++--- 2 files changed, 35 insertions(+), 5 deletions(-) diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 50975145e..cf5ca57d7 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -565,10 +565,31 @@ impl ClauseDBIF for ClauseDB { } // alives += 1; // keep += 1; - if self.clause[ci].is(FlagClause::USED) { - self.clause[ci].turn_off(FlagClause::USED); + self.clause[ci].turn_off(FlagClause::NEW_CLAUSE); + // if self.clause[ci].is(FlagClause::FORWD_LINK) + // || self.clause[ci].is(FlagClause::BCKWD_LINK) + // { + // self.clause[ci].turn_off(FlagClause::FORWD_LINK); + // self.clause[ci].turn_off(FlagClause::BCKWD_LINK); + // continue; + // } + /* let fwd: bool = self.clause[ci].is(FlagClause::FORWD_LINK); + self.clause[ci].turn_off(FlagClause::FORWD_LINK); + if self.clause[ci].is(FlagClause::BCKWD_LINK) { + self.clause[ci].turn_off(FlagClause::BCKWD_LINK); + continue; + } */ + if self.clause[ci].is(FlagClause::FORWD_LINK) + || self.clause[ci].is(FlagClause::BCKWD_LINK) + { + self.clause[ci].turn_off(FlagClause::FORWD_LINK); + self.clause[ci].turn_off(FlagClause::BCKWD_LINK); continue; } + /* let bwd: bool = self.clause[ci].is(FlagClause::BCKWD_LINK); + if bwd { + self.clause[ci].turn_off(FlagClause::BCKWD_LINK); + } */ if self.clause[ci].is(FlagClause::LEARNT) { let ClauseDB { ref mut clause, diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index db43f67be..0207854fa 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -148,10 +148,18 @@ pub fn handle_conflict( bumped.push(vi); } } - AssignReason::Implication(r) => { + AssignReason::Implication(wli) => { + let ci = wli.as_ci(); #[cfg(feature = "keep_just_used_clauses")] - cdb[r.as_ci()].turn_on(FlagClause::USED); - for l in cdb[r.as_ci()].iter() { + { + if !cdb[ci].is(FlagClause::BCKWD_LINK) { + state + .clause_generation_shift + .update(cdb[ci].is(FlagClause::NEW_CLAUSE) as u8 as f64); + } + cdb[ci].turn_on(FlagClause::BCKWD_LINK); + } + for l in cdb[ci].iter() { let vi = l.vi(); if !bumped.contains(&vi) { asg.reward_at_analysis(vi); @@ -333,6 +341,7 @@ fn conflict_analyze( } match reason { AssignReason::BinaryLink(l) => { + state.clause_generation_shift.update(0.0); let vi = l.vi(); if !asg.var(vi).is(FlagVar::CA_SEEN) { validate_vi!(vi); From 2cd2e09cea02ce6cc2dcec782fb3952fa51fd541 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 18:53:28 +0900 Subject: [PATCH 09/27] tiny changes on edge cases at var assertion --- src/solver/conflict.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 0207854fa..9abb03e4e 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -98,12 +98,13 @@ pub fn handle_conflict( // //## A NEW ASSERTION by UNIT LEARNT CLAUSE GENERATION // + let root_level = asg.root_level(); match asg.assigned(l0) { - Some(true) if asg.root_level() < asg.level(l0.vi()) => { - panic!("double assignment occured"); - // asg.lift_to_asserted(l0.vi()); + Some(true) if asg.level(l0.vi()) == root_level => { + // dbg!("double assignment occured"); + return Ok(root_level); } - Some(false) if asg.level(l0.vi()) == asg.root_level() => { + Some(false) if asg.level(l0.vi()) == root_level => { return Err(SolverError::RootLevelConflict((l0, asg.reason(l0.vi())))); } _ => { @@ -115,7 +116,7 @@ pub fn handle_conflict( let vi = l0.vi(); state.stm.handle(SolverEvent::Assert(vi)); cdb.handle(SolverEvent::Assert(vi)); - return Ok(0); + return Ok(asg.root_level()); } } } From 7e724df01280af17bd9aaf184ddaaca6399b6b0f Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 23 Sep 2024 18:54:29 +0900 Subject: [PATCH 10/27] Reflect the current status on stat variables before displaying --- src/solver/search.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solver/search.rs b/src/solver/search.rs index 37f9e6c29..99e7b848d 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -552,6 +552,8 @@ impl SolveIF for Solver { state .stm .set_span_base(state.c_lvl.get_slow() - state.b_lvl.get_slow()); + + asg.clear_asserted_literals(cdb)?; dump_stage(asg, cdb, state, &ss.previous_stage); #[cfg(feature = "rephase")] From b4202461f71bcf24991b94d0f78850f52c7bfd52 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 26 Sep 2024 08:56:34 +0900 Subject: [PATCH 11/27] Clean up framework for vibrated reduction --- src/assign/propagate.rs | 10 +++++++++- src/assign/stack.rs | 4 ++-- src/solver/conflict.rs | 21 ++++++++++----------- src/state.rs | 13 +++++-------- 4 files changed, 26 insertions(+), 22 deletions(-) diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index ff5d3510d..81d139115 100644 --- a/src/assign/propagate.rs +++ b/src/assign/propagate.rs @@ -377,7 +377,7 @@ impl PropagateIF for AssignStack { debug_assert_eq!(self.assigned(other), None); #[cfg(feature = "keep_just_used_clauses")] { - if !c.is(FlagClause::FORWD_LINK) { + if 0 < len { let b = c.is(FlagClause::NEW_CLAUSE); self.clause_generation_shift.update(b as u8 as f64); } @@ -417,6 +417,14 @@ impl PropagateIF for AssignStack { } ); debug_assert_eq!(other, c[1 - false_index]); + #[cfg(feature = "keep_just_used_clauses")] + { + if 0 < len { + let b = c.is(FlagClause::NEW_CLAUSE); + self.clause_generation_shift.update(b as u8 as f64); + } + c.turn_on(FlagClause::FORWD_LINK); + } conflict_path!( other, if len == 0 { diff --git a/src/assign/stack.rs b/src/assign/stack.rs index 8330dbf48..6a432f344 100644 --- a/src/assign/stack.rs +++ b/src/assign/stack.rs @@ -47,7 +47,7 @@ pub struct AssignStack { // //## Stage // - pub clause_generation_shift: Ema, + pub clause_generation_shift: Ema2, pub stage_scale: usize, //## Elimanated vars @@ -126,7 +126,7 @@ impl Default for AssignStack { #[cfg(feature = "rephase")] phase_age: 0, - clause_generation_shift: Ema::new(12000), + clause_generation_shift: Ema2::new(8 * 8192).with_slow(32 * 8192), stage_scale: 1, eliminated: Vec::new(), diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 9abb03e4e..7ec029dd1 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -153,11 +153,9 @@ pub fn handle_conflict( let ci = wli.as_ci(); #[cfg(feature = "keep_just_used_clauses")] { - if !cdb[ci].is(FlagClause::BCKWD_LINK) { - state - .clause_generation_shift - .update(cdb[ci].is(FlagClause::NEW_CLAUSE) as u8 as f64); - } + state + .clause_generation_shift + .update(cdb[ci].is(FlagClause::NEW_CLAUSE) as u8 as f64); cdb[ci].turn_on(FlagClause::BCKWD_LINK); } for l in cdb[ci].iter() { @@ -361,13 +359,14 @@ fn conflict_analyze( let (ci, skip) = wli.indices(); if !cdb[ci].is(FlagClause::LEARNT) { state.derive20.push(ci); - } else { - #[cfg(feature = "keep_just_used_clauses")] - cdb[ci].turn_on(FlagClause::FORWD_LINK); } - state - .clause_generation_shift - .update(cdb[ci].is(FlagClause::FORWD_LINK) as u8 as f64); + #[cfg(feature = "keep_just_used_clauses")] + { + state + .clause_generation_shift + .update(cdb[ci].is(FlagClause::NEW_CLAUSE) as u8 as f64); + cdb[ci].turn_on(FlagClause::BCKWD_LINK); + } if max_lbd < cdb[ci].rank { max_lbd = cdb[ci].rank; ci_with_max_lbd = Some(ci); diff --git a/src/state.rs b/src/state.rs index 7cba85621..1120b55c4 100644 --- a/src/state.rs +++ b/src/state.rs @@ -89,8 +89,6 @@ pub struct State { pub stm: StageManager, /// problem description pub target: CNFDescription, - /// strategy adjustment interval in conflict - pub reflection_interval: usize, // //## MISC @@ -113,7 +111,7 @@ pub struct State { pub chrono_bt_threshold: DecisionLevel, /// for clause reduction - pub clause_generation_shift: Ema, + pub clause_generation_shift: Ema2, /// hold the previous number of non-conflicting assignment pub last_asg: usize, /// working place to build learnt clauses @@ -145,11 +143,10 @@ impl Default for State { // restart: RestartManager::default(), stm: StageManager::default(), target: CNFDescription::default(), - reflection_interval: 10_000, - b_lvl: Ema2::new(16).with_slow(4_000), - c_lvl: Ema2::new(16).with_slow(4_000), - e_mode: Ema2::new(40).with_slow(4_000).with_value(10.0), + b_lvl: Ema2::new(16).with_slow(4096), + c_lvl: Ema2::new(16).with_slow(4096), + e_mode: Ema2::new(32).with_slow(4096).with_value(10.0), e_mode_threshold: 1.20, exploration_rate_ema: Ema::new(1000), @@ -159,7 +156,7 @@ impl Default for State { #[cfg(feature = "chrono_BT")] chrono_bt_threshold: 100, - clause_generation_shift: Ema::new(12000), + clause_generation_shift: Ema2::new(8 * 8192).with_slow(32 * 8129), last_asg: 0, new_learnt: Vec::new(), derive20: Vec::new(), From d7f4c5904a4de57eaf8838db7e582374cf40e7d3 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 26 Sep 2024 09:13:14 +0900 Subject: [PATCH 12/27] ditto --- src/solver/conflict.rs | 1 - src/solver/stage.rs | 6 ++---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 7ec029dd1..7bcf2d044 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -114,7 +114,6 @@ pub fn handle_conflict( unreachable!("handle_conflict::root_level_conflict_by_assertion"); } let vi = l0.vi(); - state.stm.handle(SolverEvent::Assert(vi)); cdb.handle(SolverEvent::Assert(vi)); return Ok(asg.root_level()); } diff --git a/src/solver/stage.rs b/src/solver/stage.rs index e156d94b0..03f3e3d32 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -49,10 +49,8 @@ impl Instantiate for StageManager { ..StageManager::default() } } - fn handle(&mut self, e: SolverEvent) { - if let SolverEvent::Assert(_) = e { - self.reset(); - } + fn handle(&mut self, _: SolverEvent) { + unimplemented!(); } } From d8be873c3b1b24161ec67c936fce5b09ba1ea6f4 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 26 Sep 2024 09:50:14 +0900 Subject: [PATCH 13/27] A tiny change --- src/state.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/state.rs b/src/state.rs index 1120b55c4..15f146f80 100644 --- a/src/state.rs +++ b/src/state.rs @@ -560,9 +560,9 @@ impl StateIF for State { // "\x1B[2K misc|ccut:{}, vdcy:{}, core:{}, /ppc:{}", "\x1B[2K{:>12}|ccut:{}, vdcy:{}, core:{}, /ppc:{}", format!( - "Luby{}.{:0>2}", + "Luby{:>2}.{:0>2}", self.stm.current_segment(), - ((self.stm.segment_progress_ratio() * 100.0) as usize - 1).clamp(0, 99), + ((self.stm.segment_progress_ratio() * 100.0) as usize).clamp(0, 99), ), fm!( "{:>9.4}", From b963024d43f6ac31e8840535aee78f21f015c2b9 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 28 Sep 2024 12:18:36 +0900 Subject: [PATCH 14/27] vivify: limit by the number of literals instead of clauses --- src/cdb/vivify.rs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index cf7f04f59..7252034ed 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -34,10 +34,10 @@ impl VivifyIF for ClauseDB { // 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; + let mut num_checked: usize = 0; + let mut num_shrink: usize = 0; + let mut num_assert: usize = 0; + let mut to_display: usize = 0; 'next_clause: while let Some(cp) = clauses.pop() { asg.backtrack_sandbox(); debug_assert_eq!(asg.decision_level(), asg.root_level()); @@ -56,17 +56,17 @@ impl VivifyIF for ClauseDB { let is_learnt = c.is(FlagClause::LEARNT); c.vivified(); let clits = c.iter().copied().collect::>(); - if to_display <= num_check { + if to_display <= num_checked { state.flush(""); state.flush(format!( - "clause vivifying(assert:{num_assert} shorten:{num_shrink}, check:{num_check}/{num_target})..." + "clause vivifying(assert:{num_assert} shorten:{num_shrink}, check:{num_checked}/{num_target})..." )); - to_display = num_check + display_step; + to_display = num_checked + display_step; } - num_check += 1; // debug_assert!(clits.iter().all(|l| !clits.contains(&!*l))); let mut decisions: Vec = Vec::new(); for lit in clits.iter().copied() { + num_checked += 1; // assert!(!asg.var(lit.vi()).is(FlagVar::ELIMINATED)); match asg.assigned(!lit) { //## Rule 1 @@ -94,7 +94,7 @@ impl VivifyIF for ClauseDB { continue 'next_clause; } else { debug_assert!(clits.len() != 2 || decisions.len() != 2); - seen[0] = num_check; + seen[0] = num_checked; vec = asg .analyze_sandbox(self, &decisions, &cnfl_lits, &mut seen); asg.backtrack_sandbox(); @@ -109,7 +109,7 @@ impl VivifyIF for ClauseDB { } else { let cnfl_lits = &self[wli.as_ci()].iter().copied().collect::>(); - seen[0] = num_check; + seen[0] = num_checked; vec = asg.analyze_sandbox(self, &decisions, cnfl_lits, &mut seen); asg.backtrack_sandbox(); @@ -150,7 +150,7 @@ impl VivifyIF for ClauseDB { } } } - if VIVIFY_LIMIT < num_check { + if VIVIFY_LIMIT < num_checked { break; } } From c1eccd8452f7398a7c734dda7b5df6ff54272448 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 28 Sep 2024 12:22:57 +0900 Subject: [PATCH 15/27] Fix inconsistencies on entanglement and `FlagClause::FORWD_LINK` --- src/cdb/mod.rs | 6 ++++-- src/solver/conflict.rs | 19 ++++++++++++++----- 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index cf5ca57d7..43e88a3dc 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -92,7 +92,7 @@ pub trait ClauseDBIF: fn reset(&mut self); /// update flags. /// return `true` if it's learnt. - fn update_at_analysis(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> bool; + fn update_entanglement(&mut self, asg: &impl AssignIF, ci: ClauseIndex); /// record an asserted literal to unsat certification. fn certificate_add_assertion(&mut self, lit: Lit); /// save the certification record to a file. @@ -507,7 +507,9 @@ impl ClauseDBIF for ClauseDB { // self.check_weave(wli.as_ci(), &[0, 1]); ret } - fn update_at_analysis(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> bool { + /// This function is called only on the learnt clause which has the highest LBD in + /// an analysis. + fn update_entanglement(&mut self, asg: &impl AssignIF, ci: ClauseIndex) { let ClauseDB { ref mut clause, ref mut lbd_temp, diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 7bcf2d044..6ad083caf 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -205,9 +205,6 @@ pub fn handle_conflict( assign_level, ); // || check_graph(asg, cdb, l0, "biclause"); - for cid in &state.derive20 { - cdb[*cid].turn_on(FlagClause::DERIVE20); - } rank = 1; #[cfg(feature = "bi_clause_completion")] cdb.complete_bi_clauses(asg); @@ -218,6 +215,14 @@ pub fn handle_conflict( debug_assert_eq!(cdb[cid].lit0(), l0); debug_assert_eq!(asg.assigned(l0), None); + + #[cfg(feature = "keep_just_used_clauses")] + { + let b = cdb[cid].is(FlagClause::NEW_CLAUSE); + asg.clause_generation_shift.update(b as u8 as f64); + cdb[cid].turn_on(FlagClause::FORWD_LINK); + } + asg.assign_by_implication( l0, AssignReason::Implication(WatchLiteralIndex::new(cid, 0)), @@ -359,6 +364,10 @@ fn conflict_analyze( if !cdb[ci].is(FlagClause::LEARNT) { state.derive20.push(ci); } + + #[cfg(feature = "clause_rewarding")] + cdb.reward_at_analysis(ci); + #[cfg(feature = "keep_just_used_clauses")] { state @@ -366,7 +375,7 @@ fn conflict_analyze( .update(cdb[ci].is(FlagClause::NEW_CLAUSE) as u8 as f64); cdb[ci].turn_on(FlagClause::BCKWD_LINK); } - if max_lbd < cdb[ci].rank { + if cdb[ci].is(FlagClause::LEARNT) && max_lbd < cdb[ci].rank { max_lbd = cdb[ci].rank; ci_with_max_lbd = Some(ci); } @@ -414,7 +423,7 @@ fn conflict_analyze( path_cnt -= 1; } if let Some(cid) = ci_with_max_lbd { - cdb.update_at_analysis(asg, cid); + cdb.update_entanglement(asg, cid); } minimize_learnt(&mut state.new_learnt, asg, cdb) } From 517efab129af75356201d18f8a0075c61d13a7bd Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Wed, 2 Oct 2024 18:52:41 +0900 Subject: [PATCH 16/27] fix a compile error --- src/cdb/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 43e88a3dc..3a4e945d4 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -527,7 +527,6 @@ impl ClauseDBIF for ClauseDB { if 1 < rank { self.lb_entanglement.update(rank as f64); } - learnt } /// reduce the number of 'learnt' or *removable* clauses. #[cfg(feature = "keep_just_used_clauses")] From b75c677a54dab8184056e5db9f2270dc4d05b84c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 25 Oct 2024 17:38:03 +0900 Subject: [PATCH 17/27] Update toolchains --- .envrc | 4 +- Cargo.lock | 141 ++++++++++++++++++++++++----------------------------- Cargo.toml | 2 +- 3 files changed, 66 insertions(+), 81 deletions(-) diff --git a/.envrc b/.envrc index 9ee556b10..cf034b9f7 100644 --- a/.envrc +++ b/.envrc @@ -1,4 +1,2 @@ -if ! has nix_direnv_version || ! nix_direnv_version 3.0.5; then - source_url "https://raw.githubusercontent.com/nix-community/nix-direnv/3.0.5/direnvrc" "sha256-RuwIS+QKFj/T9M2TFXScjBsLR6V3A17YVoEW/Q6AZ1w=" -fi +source $HOME/.config/direnv/envrc use flake diff --git a/Cargo.lock b/Cargo.lock index 57ec2655c..c2644ae4a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,18 +2,6 @@ # It is not intended for manual editing. version = 3 -[[package]] -name = "ahash" -version = "0.8.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" -dependencies = [ - "cfg-if", - "once_cell", - "version_check", - "zerocopy", -] - [[package]] name = "allocator-api2" version = "0.2.18" @@ -22,9 +10,9 @@ checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f" [[package]] name = "autocfg" -version = "1.3.0" +version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" +checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" [[package]] name = "bitflags" @@ -113,6 +101,12 @@ version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" +[[package]] +name = "equivalent" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" + [[package]] name = "errno" version = "0.3.9" @@ -123,14 +117,21 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "foldhash" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f81ec6369c545a7d40e4589b5597581fa1c441fe1cce96dd1de43159910a36a2" + [[package]] name = "hashbrown" -version = "0.14.5" +version = "0.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" +checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" dependencies = [ - "ahash", "allocator-api2", + "equivalent", + "foldhash", ] [[package]] @@ -145,6 +146,12 @@ version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" +[[package]] +name = "indoc" +version = "2.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" + [[package]] name = "instability" version = "0.3.2" @@ -184,18 +191,18 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "js-sys" -version = "0.3.70" +version = "0.3.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1868808506b929d7b0cfa8f75951347aa71bb21144b7791bae35d9bccfcfe37a" +checksum = "6a88f1bda2bd75b0452a14784937d796722fdebfe50df998aeb3f0b7603019a9" dependencies = [ "wasm-bindgen", ] [[package]] name = "libc" -version = "0.2.158" +version = "0.2.161" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d8adc4bb1803a324070e64a98ae98f38934d91957a99cfb3a43dcbc01bc56439" +checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" [[package]] name = "linux-raw-sys" @@ -221,9 +228,9 @@ checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" [[package]] name = "lru" -version = "0.12.4" +version = "0.12.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37ee39891760e7d94734f6f63fedc29a2e4a152f836120753a72503f09fcf904" +checksum = "234cf4f4a04dc1f57e24b96cc0cd600cf2af460d4161ac5ecdd0af8e1f3b2a38" dependencies = [ "hashbrown", ] @@ -258,9 +265,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.19.0" +version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" +checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "parking_lot" @@ -299,9 +306,9 @@ checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" [[package]] name = "proc-macro2" -version = "1.0.86" +version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" +checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" dependencies = [ "unicode-ident", ] @@ -317,31 +324,31 @@ dependencies = [ [[package]] name = "ratatui" -version = "0.28.1" +version = "0.29.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fdef7f9be5c0122f890d58bdf4d964349ba6a6161f705907526d891efabba57d" +checksum = "eabd94c2f37801c20583fc49dd5cd6b0ba68c716787c2dd6ed18571e1e63117b" dependencies = [ "bitflags", "cassowary", "compact_str", "crossterm", + "indoc", "instability", "itertools", "lru", "paste", "strum", - "strum_macros", "time", "unicode-segmentation", "unicode-truncate", - "unicode-width", + "unicode-width 0.2.0", ] [[package]] name = "redox_syscall" -version = "0.5.4" +version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0884ad60e090bf1345b93da0a5de8923c93884cd03f40dfcfddd3b4bee661853" +checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" dependencies = [ "bitflags", ] @@ -361,9 +368,9 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "955d28af4278de8121b7ebeb796b6a45735dc01436d898801014aced2773a3d6" +checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" [[package]] name = "ryu" @@ -379,18 +386,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.210" +version = "1.0.213" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a" +checksum = "3ea7893ff5e2466df8d720bb615088341b295f849602c6956047f8f80f0e9bc1" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.210" +version = "1.0.213" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" +checksum = "7e85ad2009c50b58e87caa8cd6dac16bdf511bbfb7af6c33df902396aa480fa5" dependencies = [ "proc-macro2", "quote", @@ -473,9 +480,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.77" +version = "2.0.85" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed" +checksum = "5023162dfcd14ef8f32034d8bcd4cc5ddc61ef7a247c024a33e24e1f24d21b56" dependencies = [ "proc-macro2", "quote", @@ -523,7 +530,7 @@ checksum = "b3644627a5af5fa321c95b9b235a72fd24cd29c648c2c379431e6628655627bf" dependencies = [ "itertools", "unicode-segmentation", - "unicode-width", + "unicode-width 0.1.14", ] [[package]] @@ -533,10 +540,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" [[package]] -name = "version_check" -version = "0.9.5" +name = "unicode-width" +version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +checksum = "1fc81956842c57dac11422a97c3b8195a1ff727f06e85c84ed2e8aa277c9a0fd" [[package]] name = "wasi" @@ -546,9 +553,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a82edfc16a6c469f5f44dc7b571814045d60404b55a0ee849f9bcfa2e63dd9b5" +checksum = "128d1e363af62632b8eb57219c8fd7877144af57558fb2ef0368d0087bddeb2e" dependencies = [ "cfg-if", "once_cell", @@ -557,9 +564,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9de396da306523044d3302746f1208fa71d7532227f15e347e2d93e4145dd77b" +checksum = "cb6dd4d3ca0ddffd1dd1c9c04f94b868c37ff5fac97c30b97cff2d74fce3a358" dependencies = [ "bumpalo", "log", @@ -572,9 +579,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "585c4c91a46b072c92e908d99cb1dcdf95c5218eeb6f3bf1efa991ee7a68cccf" +checksum = "e79384be7f8f5a9dd5d7167216f022090cf1f9ec128e6e6a482a2cb5c5422c56" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -582,9 +589,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "afc340c74d9005395cf9dd098506f7f44e38f2b4a21c6aaacf9a105ea5e1e836" +checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" dependencies = [ "proc-macro2", "quote", @@ -595,15 +602,15 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c62a0a307cb4a311d3a07867860911ca130c3494e8c2719593806c08bc5d0484" +checksum = "65fc09f10666a9f147042251e0dda9c18f166ff7de300607007e96bdebc1068d" [[package]] name = "web-sys" -version = "0.3.70" +version = "0.3.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26fdeaafd9bd129f65e7c031593c24d62186301e0c72c8978fa1678be7d532c0" +checksum = "f6488b90108c040df0fe62fa815cbdee25124641df01814dd7282749234c6112" dependencies = [ "js-sys", "wasm-bindgen", @@ -703,23 +710,3 @@ name = "windows_x86_64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" - -[[package]] -name = "zerocopy" -version = "0.7.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" -dependencies = [ - "zerocopy-derive", -] - -[[package]] -name = "zerocopy-derive" -version = "0.7.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] diff --git a/Cargo.toml b/Cargo.toml index 199256eb4..ba55a88a0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -19,7 +19,7 @@ bitflags = "^2.6" instant = { version = "0.1", features = ["wasm-bindgen"], optional = true } crossterm = { version = "^0.28", optional = true } -ratatui = { version = "^0.28", features = ["all-widgets"], optional = true } +ratatui = { version = "^0.29", features = ["all-widgets"], optional = true } [features] default = [ From 6d9b1106dac9ac82f6ee70ca61658196901a091f Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 7 Nov 2024 23:07:17 +0900 Subject: [PATCH 18/27] Update toolchain --- Cargo.lock | 34 ++++++++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c2644ae4a..c5e2e4b1a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -125,9 +125,15 @@ checksum = "f81ec6369c545a7d40e4589b5597581fa1c441fe1cce96dd1de43159910a36a2" [[package]] name = "hashbrown" +<<<<<<< HEAD version = "0.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" +======= +version = "0.15.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" +>>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "allocator-api2", "equivalent", @@ -200,9 +206,15 @@ dependencies = [ [[package]] name = "libc" +<<<<<<< HEAD version = "0.2.161" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" +======= +version = "0.2.162" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398" +>>>>>>> 0a8bb833 (Update toolchain) [[package]] name = "linux-raw-sys" @@ -355,9 +367,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.37" +version = "0.38.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8acb788b847c24f28525660c4d7758620a7210875711f79e7f663cc152726811" +checksum = "375116bee2be9ed569afe2154ea6a99dfdffd257f533f187498c2a8f5feaf4ee" dependencies = [ "bitflags", "errno", @@ -386,18 +398,30 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" +<<<<<<< HEAD version = "1.0.213" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3ea7893ff5e2466df8d720bb615088341b295f849602c6956047f8f80f0e9bc1" +======= +version = "1.0.214" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5" +>>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" +<<<<<<< HEAD version = "1.0.213" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7e85ad2009c50b58e87caa8cd6dac16bdf511bbfb7af6c33df902396aa480fa5" +======= +version = "1.0.214" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766" +>>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "proc-macro2", "quote", @@ -480,9 +504,15 @@ dependencies = [ [[package]] name = "syn" +<<<<<<< HEAD version = "2.0.85" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5023162dfcd14ef8f32034d8bcd4cc5ddc61ef7a247c024a33e24e1f24d21b56" +======= +version = "2.0.87" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" +>>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "proc-macro2", "quote", From 07c46f6d06d129b588ff01c7af9002c0aee0a9a2 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 7 Nov 2024 23:42:37 +0900 Subject: [PATCH 19/27] modified: flake.lock --- flake.lock | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/flake.lock b/flake.lock index 4326e0e47..dc7345de3 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "nixpkgs": { "locked": { - "lastModified": 1726227518, - "narHash": "sha256-i4b4IcHBiukSgUP875FLe9x/wrWns7AJuj8+8VuqpFU=", + "lastModified": 1730989260, + "narHash": "sha256-5R9m921OhgOUNHVIxTS8+jZJokkZRsH7UOecxlchqZ8=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "da8415506ffd6c72680825595bfee80ebbe06128", + "rev": "3aea494127aae5d08c4c501ea4ba27e6c185b822", "type": "github" }, "original": { @@ -17,11 +17,11 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1724467107, - "narHash": "sha256-oZW7ymnqv9yyd6Ey04j/fjp+X7kayKEpBUbnAHlcGU4=", + "lastModified": 1730988789, + "narHash": "sha256-Yx1f4uPcvel/iv9sbx60lVS8oihlgN+qeUuMZ3T4Vvc=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "0b6fa5ee40c14df33494d4ed9da1251e872fb0c2", + "rev": "c1612975107c932f1e903d8fab1636334402c6d2", "type": "github" }, "original": { @@ -41,11 +41,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1725558991, - "narHash": "sha256-4RcUUEq29/t0i+awEuUngPC2f4QuscVgAGeFDD5HM3s=", + "lastModified": 1730990089, + "narHash": "sha256-9E+GA8WYLSvfRughvLsz35mu1NkNvKD0RGw6X3OTgkw=", "owner": "shnarazk", "repo": "SAT-bench", - "rev": "1923148519d315228021fc015edd4e42394adcf2", + "rev": "30cddaa30105081ab0c0fb3713cea04eb82053f2", "type": "github" }, "original": { From 0a8280ed31e5806cb8c42ea193a4d2a40f772945 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 7 Nov 2024 23:44:16 +0900 Subject: [PATCH 20/27] modified: Cargo.lock --- Cargo.lock | 30 ------------------------------ 1 file changed, 30 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c5e2e4b1a..bfdf07fbc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -125,15 +125,9 @@ checksum = "f81ec6369c545a7d40e4589b5597581fa1c441fe1cce96dd1de43159910a36a2" [[package]] name = "hashbrown" -<<<<<<< HEAD -version = "0.15.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" -======= version = "0.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" ->>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "allocator-api2", "equivalent", @@ -206,15 +200,9 @@ dependencies = [ [[package]] name = "libc" -<<<<<<< HEAD -version = "0.2.161" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" -======= version = "0.2.162" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398" ->>>>>>> 0a8bb833 (Update toolchain) [[package]] name = "linux-raw-sys" @@ -398,30 +386,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -<<<<<<< HEAD -version = "1.0.213" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3ea7893ff5e2466df8d720bb615088341b295f849602c6956047f8f80f0e9bc1" -======= version = "1.0.214" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5" ->>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -<<<<<<< HEAD -version = "1.0.213" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e85ad2009c50b58e87caa8cd6dac16bdf511bbfb7af6c33df902396aa480fa5" -======= version = "1.0.214" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766" ->>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "proc-macro2", "quote", @@ -504,15 +480,9 @@ dependencies = [ [[package]] name = "syn" -<<<<<<< HEAD -version = "2.0.85" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5023162dfcd14ef8f32034d8bcd4cc5ddc61ef7a247c024a33e24e1f24d21b56" -======= version = "2.0.87" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" ->>>>>>> 0a8bb833 (Update toolchain) dependencies = [ "proc-macro2", "quote", From 833a25280b7ac97832d8d89f3df2cd09f5484a29 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 14 Nov 2024 10:04:48 +0900 Subject: [PATCH 21/27] Update toolchains --- Cargo.lock | 99 ++++++++++++++++++++++++++++++++++++++++++++++++------ flake.nix | 1 - 2 files changed, 89 insertions(+), 11 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index bfdf07fbc..a02f99dee 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "allocator-api2" -version = "0.2.18" +version = "0.2.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f" +checksum = "45862d1c77f2228b9e10bc609d5bc203d86ebc9b87ad8d5d5167a6c9abf739d9" [[package]] name = "autocfg" @@ -86,6 +86,41 @@ dependencies = [ "winapi", ] +[[package]] +name = "darling" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f63b86c8a8826a49b8c21f08a2d07338eec8d900540f8630dc76284be802989" +dependencies = [ + "darling_core", + "darling_macro", +] + +[[package]] +name = "darling_core" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "95133861a8032aaea082871032f5815eb9e98cef03fa916ab4500513994df9e5" +dependencies = [ + "fnv", + "ident_case", + "proc-macro2", + "quote", + "strsim", + "syn", +] + +[[package]] +name = "darling_macro" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d336a2a514f6ccccaa3e09b02d41d35330c07ddf03a62165fcec10bb561c7806" +dependencies = [ + "darling_core", + "quote", + "syn", +] + [[package]] name = "deranged" version = "0.3.11" @@ -95,6 +130,12 @@ dependencies = [ "powerfmt", ] +[[package]] +name = "diff" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "56254986775e3233ffa9c4d7d3faaf6d36a2c09d30b20687e9f88bc8bafc16c8" + [[package]] name = "either" version = "1.13.0" @@ -117,6 +158,12 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + [[package]] name = "foldhash" version = "0.1.3" @@ -146,6 +193,12 @@ version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" +[[package]] +name = "ident_case" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" + [[package]] name = "indoc" version = "2.0.5" @@ -154,10 +207,14 @@ checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" [[package]] name = "instability" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b23a0c8dfe501baac4adf6ebbfa6eddf8f0c07f56b058cc1288017e32397846c" +checksum = "b829f37dead9dc39df40c2d3376c179fdfd2ac771f53f55d3c30dc096a3c0c6e" dependencies = [ + "darling", + "indoc", + "pretty_assertions", + "proc-macro2", "quote", "syn", ] @@ -304,6 +361,16 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" +[[package]] +name = "pretty_assertions" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3ae130e2f271fbc2ac3a40fb1d07180839cdbbe443c7a27e1e3c13c5cac0116d" +dependencies = [ + "diff", + "yansi", +] + [[package]] name = "proc-macro2" version = "1.0.89" @@ -355,9 +422,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.39" +version = "0.38.40" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "375116bee2be9ed569afe2154ea6a99dfdffd257f533f187498c2a8f5feaf4ee" +checksum = "99e4ea3e1cdc4b559b8e5650f9c8e5998e3e5c1343b4eaf034565f32318d63c0" dependencies = [ "bitflags", "errno", @@ -386,18 +453,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.214" +version = "1.0.215" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5" +checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.214" +version = "1.0.215" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766" +checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" dependencies = [ "proc-macro2", "quote", @@ -456,6 +523,12 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" +[[package]] +name = "strsim" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" + [[package]] name = "strum" version = "0.26.3" @@ -710,3 +783,9 @@ name = "windows_x86_64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" + +[[package]] +name = "yansi" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfe53a6657fd280eaa890a3bc59152892ffa3e30101319d168b781ed6529b049" diff --git a/flake.nix b/flake.nix index 82f383ca8..cdcc45a19 100644 --- a/flake.nix +++ b/flake.nix @@ -39,7 +39,6 @@ value = mkShell { packages = [ bashInteractive - libiconv samply tokei # cargo-watch From 9f1d31baf0b2bebab6fcba24cf04f67ead6625d3 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 15 Nov 2024 00:35:44 +0900 Subject: [PATCH 22/27] Vivification delete clauses if possible (resolved #272) --- src/cdb/vivify.rs | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index 7252034ed..ff0794ff8 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -36,6 +36,7 @@ impl VivifyIF for ClauseDB { let display_step: usize = 1000; let mut num_checked: usize = 0; let mut num_shrink: usize = 0; + let mut num_subsumed: usize = 0; let mut num_assert: usize = 0; let mut to_display: usize = 0; 'next_clause: while let Some(cp) = clauses.pop() { @@ -59,7 +60,7 @@ impl VivifyIF for ClauseDB { if to_display <= num_checked { state.flush(""); state.flush(format!( - "clause vivifying(assert:{num_assert} shorten:{num_shrink}, check:{num_checked}/{num_target})..." + "vivifying(assert:{num_assert} subsume:{num_subsumed}, shorten:{num_shrink}, check:{num_checked}/{num_target})..." )); to_display = num_checked + display_step; } @@ -101,6 +102,18 @@ impl VivifyIF for ClauseDB { } } AssignReason::Implication(wli) => { + if wli.as_ci() != ci + && is_learnt + && decisions.len() <= clits.len() + && self.clause[wli.as_ci()].len() <= clits.len() + { + assert!(!self.clause[wli.as_ci()].is_dead()); + assert!(!self.clause[ci].is_dead()); + asg.backtrack_sandbox(); + self.delete_clause(ci); + num_subsumed += 1; + continue 'next_clause; + } if wli.as_ci() == ci && clits.len() == decisions.len() { // #[cfg(feature = "keep_just_used_clauses")] // self.clause[ci].turn_on(FlagClause::??); @@ -163,7 +176,7 @@ impl VivifyIF for ClauseDB { debug_assert!(asg.stack_is_empty() || !asg.remains()); state.flush(""); state.flush(format!( - "vivification(assert:{num_assert} shorten:{num_shrink}), " + "vivified(assert:{num_assert}, subsume:{num_subsumed}, shorten:{num_shrink}), " )); // state.log( // asg.num_conflict, @@ -355,7 +368,7 @@ impl Clause { (!self.is_dead() && self.rank * 2 <= self.rank_old && (self.is(FlagClause::LEARNT) || self.is(FlagClause::DERIVE20))) - .then(|| -((self.rank_old - self.rank) as f64 / self.rank as f64)) + .then(|| (self.rank_old - self.rank) as f64 / self.rank as f64) } } /// clear flags about vivification From efb037b1fc497b5dedb305759b81b6a3f4ceb342 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 15 Nov 2024 01:10:50 +0900 Subject: [PATCH 23/27] Change the definition of clause entanglement --- src/cdb/db.rs | 5 +---- src/cdb/mod.rs | 24 ++++-------------------- src/solver/conflict.rs | 4 ++-- 3 files changed, 7 insertions(+), 26 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index f2724876e..1414b2d86 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -164,10 +164,7 @@ impl Instantiate for ClauseDB { self.watch.push(WatchLiteralIndexRef::default()); self.lbd_temp.push(0); } - SolverEvent::Restart => { - // self.lbd.reset_to(self.lb_entanglement.get()); - // self.lbd.reset_to(0.0); - } + SolverEvent::Restart => (), _ => (), } } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 3a4e945d4..466a52c91 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -164,8 +164,7 @@ impl Default for ClauseDB { num_learnt: 0, num_reduction: 0, num_reregistration: 0, - // lb_entanglement: Ema2::new(1_000).with_slow(80_000).with_value(16.0), - lb_entanglement: Ema2::new(16).with_slow(8192).with_value(16.0), + lb_entanglement: Ema2::new(256).with_slow(8192).with_value(16.0), #[cfg(all(feature = "clause_elimination", not(feature = "incremental_solver")))] eliminated_permanent: Vec::new(), @@ -507,8 +506,8 @@ impl ClauseDBIF for ClauseDB { // self.check_weave(wli.as_ci(), &[0, 1]); ret } - /// This function is called only on the learnt clause which has the highest LBD in - /// an analysis. + // The entanglement is defined as the average on max LBDs + // of which clauses are used conflict analysis fn update_entanglement(&mut self, asg: &impl AssignIF, ci: ClauseIndex) { let ClauseDB { ref mut clause, @@ -517,16 +516,7 @@ impl ClauseDBIF for ClauseDB { } = self; let c = &mut clause[ci]; let rank: DecisionLevel = c.update_lbd(asg, lbd_temp); - let learnt = c.is(FlagClause::LEARNT); - if learnt { - #[cfg(feature = "keep_just_used_clauses")] - c.turn_on(FlagClause::NEW_CLAUSE); - #[cfg(feature = "clause_rewarding")] - self.reward_at_analysis(ci); - } - if 1 < rank { - self.lb_entanglement.update(rank as f64); - } + self.lb_entanglement.update(rank as f64); } /// reduce the number of 'learnt' or *removable* clauses. #[cfg(feature = "keep_just_used_clauses")] @@ -554,12 +544,6 @@ impl ClauseDBIF for ClauseDB { // let mut alives: usize = 0; // let mut perm: Vec> = Vec::with_capacity(clause.len()); // let reduction_threshold = self.reduction_threshold + 4; - /* let reduction_threshold: DecisionLevel = 4 - + ((self - .reduction_threshold - .saturating_sub(self.lb_entanglement.get() as u32) - + 1) as f64) - .sqrt() as u32; */ for ci in 1..self.clause.len() { if self.clause[ci].is_dead() { continue; diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 6ad083caf..3d6963139 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -359,7 +359,6 @@ fn conflict_analyze( p ); debug_assert!(2 < cdb[wli.as_ci()].len()); - // if !cdb.update_at_analysis(asg, cid) { let (ci, skip) = wli.indices(); if !cdb[ci].is(FlagClause::LEARNT) { state.derive20.push(ci); @@ -375,7 +374,8 @@ fn conflict_analyze( .update(cdb[ci].is(FlagClause::NEW_CLAUSE) as u8 as f64); cdb[ci].turn_on(FlagClause::BCKWD_LINK); } - if cdb[ci].is(FlagClause::LEARNT) && max_lbd < cdb[ci].rank { + + if max_lbd < cdb[ci].rank { max_lbd = cdb[ci].rank; ci_with_max_lbd = Some(ci); } From d5dfed2765b318a0ea3bbcd09d1f03745a901f89 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 15 Nov 2024 10:02:51 +0900 Subject: [PATCH 24/27] Vivification can remove given clauses --- src/cdb/vivify.rs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index ff0794ff8..d2a178f24 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -102,15 +102,17 @@ impl VivifyIF for ClauseDB { } } AssignReason::Implication(wli) => { - if wli.as_ci() != ci - && is_learnt - && decisions.len() <= clits.len() - && self.clause[wli.as_ci()].len() <= clits.len() + if wli.as_ci() != ci && decisions.len() <= clits.len() + // && self.clause[wli.as_ci()].len() <= clits.len() { - assert!(!self.clause[wli.as_ci()].is_dead()); - assert!(!self.clause[ci].is_dead()); + debug_assert!(!self.clause[wli.as_ci()].is_dead()); + debug_assert!(!self.clause[ci].is_dead()); asg.backtrack_sandbox(); self.delete_clause(ci); + if !is_learnt && self.clause[wli.as_ci()].is(FlagClause::LEARNT) + { + self.clause[wli.as_ci()].turn_off(FlagClause::LEARNT); + } num_subsumed += 1; continue 'next_clause; } From 7f7f7b14da189dab763ecc5ece4b5348ba69a193 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 15 Nov 2024 10:04:17 +0900 Subject: [PATCH 25/27] Change dynamics of var decay rate --- src/solver/search.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index 99e7b848d..f879c6d54 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -508,17 +508,17 @@ impl SolveIF for Solver { let n: f64 = stm.current_cycle() as f64 - b; if cfg!(feature = "reward_annealing") { - const SLOP: f64 = 2.0; - let sgm = |x: f64| x / (1.0 + x.abs()); - let m: f64 = 0.5 * b; let k: f64 = (stm.current_segment() as f64).log2(); - const R: (f64, f64) = (0.86, 0.995); - let d: f64 = { - let o: f64 = SLOP; - R.1 - (R.1 - R.0) * o / (k + o) + let ratio: f64 = stm.segment_progress_ratio(); + const SLOP: f64 = 8.0; + const R: (f64, f64) = (0.84, 0.995); + let d: f64 = R.1 - (R.1 - R.0) * SLOP / (k + SLOP); + let x: f64 = k * (2.0 * ratio - 1.0); + let r = { + let sgm = |x: f64| 1.0 / (1.0 + (-x).exp()); + d + sgm(x) * (1.0 - d) }; - let x: f64 = (1.0 + k) * (n - m) / m; - asg.update_activity_decay(1.0 + 0.5 * (sgm(x) - 1.0) * (1.0 - d)); + asg.update_activity_decay(r); } let num_restart = asg.derefer(assign::Tusize::NumRestart); From a057b5806e6182c53a99e3b5a6b9e80cf2aed7ab Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 10 Jan 2025 14:40:11 +0900 Subject: [PATCH 26/27] cargo clippy (1.84) --- src/assign/mod.rs | 4 ++-- src/cdb/clause.rs | 5 +++++ src/cdb/mod.rs | 7 ------- src/processor/mod.rs | 2 +- src/processor/simplify.rs | 12 ++++++------ 5 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/assign/mod.rs b/src/assign/mod.rs index 92e801865..badd53734 100644 --- a/src/assign/mod.rs +++ b/src/assign/mod.rs @@ -1,5 +1,5 @@ -/// Module `assign` implements Boolean Constraint Propagation and decision var selection. -/// This version can handle Chronological and Non Chronological Backtrack. +// Module `assign` implements Boolean Constraint Propagation and decision var selection. +// This version can handle Chronological and Non Chronological Backtrack. /// Ema mod ema; diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs index cbeb0a768..2f48981f9 100644 --- a/src/cdb/clause.rs +++ b/src/cdb/clause.rs @@ -333,4 +333,9 @@ impl Clause { } self.rank } + pub fn extended_lbd(&self) -> f64 { + let l: f64 = self.len() as f64; + let r: f64 = self.rank as f64; + r + (l - r) / (l - r + 1.0) + } } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 466a52c91..78a869fb8 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -521,13 +521,6 @@ impl ClauseDBIF for ClauseDB { /// reduce the number of 'learnt' or *removable* clauses. #[cfg(feature = "keep_just_used_clauses")] fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64) { - impl Clause { - fn extended_lbd(&self) -> f64 { - let l: f64 = self.len() as f64; - let r: f64 = self.rank as f64; - r + (l - r) / (l - r + 1.0) - } - } // let ClauseDB { // ref mut clause, // ref mut lbd_temp, diff --git a/src/processor/mod.rs b/src/processor/mod.rs index 61b179c26..afe79ac0a 100644 --- a/src/processor/mod.rs +++ b/src/processor/mod.rs @@ -41,7 +41,7 @@ use { /// use crate::{splr::config::Config, splr::types::*}; /// use crate::splr::processor::{Eliminator, EliminateIF}; /// use crate::splr::solver::Solver; - +/// /// let mut s = Solver::instantiate(&Config::default(), &CNFDescription::default()); /// let mut elim = Eliminator::instantiate(&s.state.config, &s.state.cnf); /// assert_eq!(elim.is_running(), false); diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs index aa288c214..9cc097344 100644 --- a/src/processor/simplify.rs +++ b/src/processor/simplify.rs @@ -510,9 +510,9 @@ impl Eliminator { self.enqueue_var(asg, l.vi(), true); } - /// - /// clause queue operations - /// + // + // clause queue operations + // /// enqueue a clause into eliminator's clause queue. pub fn enqueue_clause(&mut self, ci: ClauseIndex, c: &mut Clause) { @@ -537,9 +537,9 @@ impl Eliminator { self.clause_queue.len() } - /// - /// var queue operations - /// + // + // var queue operations + // /// clear eliminator's var queue fn clear_var_queue(&mut self, asg: &mut impl AssignIF) { From 617d84791e595b92e38f4d67c92bfdb97f513a3c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 11 Jan 2025 15:13:31 +0900 Subject: [PATCH 27/27] a snapshot after some simplification --- src/cdb/mod.rs | 5 ++++- src/solver/search.rs | 36 +++++++++++++++++++++++------------- src/solver/stage.rs | 22 +++++++++++++++------- 3 files changed, 42 insertions(+), 21 deletions(-) diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 78a869fb8..81c419312 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -543,7 +543,10 @@ impl ClauseDBIF for ClauseDB { } // alives += 1; // keep += 1; - self.clause[ci].turn_off(FlagClause::NEW_CLAUSE); + if self.clause[ci].is(FlagClause::NEW_CLAUSE) { + self.clause[ci].turn_off(FlagClause::NEW_CLAUSE); + // continue; + } // if self.clause[ci].is(FlagClause::FORWD_LINK) // || self.clause[ci].is(FlagClause::BCKWD_LINK) // { diff --git a/src/solver/search.rs b/src/solver/search.rs index f879c6d54..df195d29f 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -497,48 +497,58 @@ impl SolveIF for Solver { #[cfg(feature = "trace_equivalency")] cdb.check_consistency(asg, "before simplify"); } - ss.current_span = state.stm.current_span() as usize; + let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow(); + let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow(); + ss.current_span = ent.max(lbd) as usize; + // ss.current_span = state.stm.current_span() as usize; let scale = state.stm.current_scale(); asg.handle(SolverEvent::Stage(scale)); if let Some(new_segment) = next_stage { // a beginning of a new cycle { - let stm = &state.stm; - let b: f64 = stm.segment_starting_cycle() as f64; - let n: f64 = stm.current_cycle() as f64 - b; + // let stm = &state.stm; + // let b: f64 = stm.segment_starting_cycle() as f64; + // let n: f64 = stm.current_cycle() as f64 - b; if cfg!(feature = "reward_annealing") { + // const_R: (f64, f64) = (0.94, 0.99); + // let k = stm.current_segment().ilog2() as f64; + // let ratio = k / (k + 1.0); + // let _ratio: f64 = stm.segment_progress_ratio(); + + // let _r = R.0 + ratio * (R.1 - R.0); + /* let k: f64 = (stm.current_segment() as f64).log2(); - let ratio: f64 = stm.segment_progress_ratio(); const SLOP: f64 = 8.0; - const R: (f64, f64) = (0.84, 0.995); let d: f64 = R.1 - (R.1 - R.0) * SLOP / (k + SLOP); let x: f64 = k * (2.0 * ratio - 1.0); let r = { let sgm = |x: f64| 1.0 / (1.0 + (-x).exp()); d + sgm(x) * (1.0 - d) }; - asg.update_activity_decay(r); + */ + asg.update_activity_decay(0.98); } let num_restart = asg.derefer(assign::Tusize::NumRestart); if ss.next_reduce <= num_restart { - 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) / (1.0 + n).log2(); + // 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.75 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2(); + let val = 5.0; state.reduction_threshold = val; cdb.reduce(asg, val); ss.num_reduction += 1; ss.reduce_step += 1; ss.next_reduce = ss.reduce_step + num_restart; - if cfg!(feature = "clause_vivification") { + if cfg!(feature = "clause_vivification") && ss.num_reduction % 8 == 0 { cdb.vivify(asg, state)?; } if cfg!(feature = "clause_elimination") && !cfg!(feature = "incremental_solver") - && ss.num_reduction % 8 == 0 + && ss.num_reduction % 15 == 0 { let mut elim = Eliminator::instantiate(&state.config, &state.cnf); state.flush("clause subsumption, "); diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 03f3e3d32..bcc843c32 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -45,7 +45,7 @@ impl Instantiate for StageManager { scale: 1, end_of_stage: unit_size, next_is_new_segment: false, - span_ema: Ema::new(4).with_value(1.0), + span_ema: Ema::new(64).with_value(1.0), ..StageManager::default() } } @@ -71,7 +71,7 @@ impl StageManager { segment_starting_stage: 0, segment_starting_cycle: 0, span_base: 0.0, - span_ema: Ema::new(4).with_value(1.0), + span_ema: Ema::new(64).with_value(1.0), } } pub fn initialize(&mut self, _unit_size: usize) { @@ -103,7 +103,8 @@ impl StageManager { let mut new_cycle = false; let mut new_segment = false; self.scale = self.generator.next_number(); - self.span_ema.update(4.0 + (self.scale as f64).powf(0.4)); + // self.span_ema.update(4.0 + (self.scale as f64).powf(0.4)); + self.span_ema.update(self.scale as f64); self.stage += 1; if self.scale == 1 { self.cycle += 1; @@ -131,22 +132,29 @@ impl StageManager { self.end_of_stage as i32 - now as i32 } /// returns the number of conflicts in the current stage + /// that was used as the number of conflicts that corresponds to the current stage /// Note: we need not to make a strong correlation between this value and /// scale defined by Luby series. So this is fine. + /// stage -> cycle -> segment pub fn current_span(&self) -> f64 { self.span_ema.get() } + /// returns the scaling factor, or length corresponding to the current stage + /// stage -> cycle -> segment + pub fn current_scale(&self) -> usize { + self.scale + } + /// return the index of the current stage /// stage -> cycle -> segment pub fn current_stage(&self) -> usize { self.stage } + /// return the index of the current cycle + /// stage -> cycle -> segment pub fn current_cycle(&self) -> usize { self.cycle } - /// returns the scaling factor used in the current span - pub fn current_scale(&self) -> usize { - self.scale - } /// returns the current index for the level 2 segments + /// stage -> cycle -> segment pub fn current_segment(&self) -> usize { self.segment }