Refine clause reduction and vivification

src/assign/mod.rs

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

src/assign/propagate.rs

@@ -206,7 +206,7 @@ impl PropagateIF for AssignStack {
                 self.var[l.vi()].assign.is_some(),
                 "cancel_until found unassigned var in trail {}{:?}",
                 l.vi(),
-                &self.var[l.vi()],
+                self.var[l.vi()],
             );
             let vi = l.vi();
             #[cfg(feature = "trace_propagation")]
@@ -251,7 +251,7 @@ impl PropagateIF for AssignStack {
                             RephaseTarget::Random => self.rng.next_bool(),
                             RephaseTarget::Inverted => !v.assign.unwrap(),
                             RephaseTarget::Polarity => {
-                                if self.rng.next_f64() <= v.polarity.abs().powf(1.1) {
+                                if self.rng.next_f64() <= v.polarity.abs().powf(1.2) {
                                     v.assign.unwrap()
                                 } else {
                                     !v.assign.unwrap()

src/assign/stack.rs

@@ -204,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]
     }
@@ -387,7 +390,7 @@ impl fmt::Display for AssignStack {
                 f,
                 "ASG:: trail({}):[(0, {:?})]\n      level: {}, asserted: {}, eliminated: {}",
                 self.trail.len(),
-                &v,
+                v,
                 levels,
                 self.num_asserted_vars,
                 self.num_eliminated_vars,

src/bin/dmcr.rs

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

src/cdb/db.rs

@@ -1,13 +1,11 @@
-use crate::assign;
-
 use {
     super::{
         BinaryLinkDB, CertificationStore, ClauseDBIF, ClauseId, RefClause,
         binary::{BinaryLinkIF, BinaryLinkList},
         property,
         watch_cache::*,
     },
-    crate::{assign::AssignIF, types::*},
+    crate::{assign::AssignIF, state::State, types::*},
     std::{
         collections::HashMap,
         num::NonZeroU32,
@@ -16,6 +14,7 @@ use {
     },
 };
 
+use std::f64;
 #[cfg(not(feature = "no_IO"))]
 use std::{fs::File, io::Write, path::Path};
 
@@ -68,7 +67,6 @@ pub struct ClauseDB {
     pub(crate) tier1_clauses: Ema,
     /// the ratio of pretty good learnt clauses
     pub(crate) tier2_clauses: Ema,
-    pub(crate) last_reduction_at: usize,
 }
 
 impl Default for ClauseDB {
@@ -91,7 +89,6 @@ impl Default for ClauseDB {
             num_reregistration: 0,
             tier1_clauses: Ema::default(),
             tier2_clauses: Ema::default(),
-            last_reduction_at: 0,
         }
     }
 }
@@ -313,11 +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;
-            c.vivify_at = 0;
         } else {
             cid = ClauseId::from(self.clause.len());
             let mut c = Clause {
@@ -339,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 {
@@ -831,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) {
+    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,
@@ -846,41 +851,38 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         *num_lbd2 = 0;
-        let num_conflict = asg.derefer(assign::property::Tusize::NumConflict);
         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 = 10_000;
-        let mut cands: Vec<SortKey<usize>> = Vec::new();
-        let thr: f64 = 1.0;
-        let scale: f64 = 2.0;
-        let cutoff: DecisionLevel = 3;
+        let mut ntier2: usize = 0;
         for (i, c) in clause
             .iter_mut()
             .enumerate()
             .skip(1)
             .filter(|(_, c)| !c.is_dead())
         {
             num_alives += 1;
-            c.update_reference_rate(num_conflict);
-            match c.lbd {
-                0..=2 => {
-                    *num_lbd2 += 1;
-                    continue;
-                }
-                n @ (3..=5) if c.reference_rate >= scale.powf((n - cutoff) as f64) * thr => {
-                    ntier1 += 1;
-                    continue;
-                }
-                _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => {
-                    continue;
-                }
-                n @ (6..) if c.reference_rate >= scale.powf((n - cutoff) as f64) * thr => {
-                    cands.push(SortKey::new(i, c.len() as f64));
-                    continue;
+            if !c.is(FlagClause::LEARNT) {
+                *num_lbd2 += (c.lbd <= 2) as usize;
+                continue;
+            }
+            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;
+            }
+            // 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(
                 certification_store,
@@ -893,72 +895,7 @@ impl ClauseDBIF for ClauseDB {
                 c,
             );
             freelist.push(ClauseId::from(i));
-            /* match c.len() {
-                0..=5 => {
-                    *num_lbd2 += 1;
-                    continue;
-                }
-                6..=8 if c.reference_rate >= 0.0001 => {
-                    ntier1 += 1;
-                    continue;
-                }
-                9 | 10 if c.reference_rate >= 0.001 => {
-                    ntier2 += 1;
-                    continue;
-                }
-                11 | 12 if c.reference_rate >= 0.01 => {
-                    ntier2 += 1;
-                    continue;
-                }
-                _ if c.lbd <= 6 && c.reference_rate >= 1.0 => {
-                    continue;
-                }
-                _ if c.referred_at >= *last_reduction_at /* && referred */ => {
-                    continue;
-                }
-                _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => {
-                    continue;
-                }
-                _ => {
-                    remove_clause_fn(
-                        certification_store,
-                        binary_link,
-                        watch_cache,
-                        num_bi_clause,
-                        num_clause,
-                        num_learnt,
-                        ClauseId::from(i),
-                        c,
-                    );
-                    freelist.push(ClauseId::from(i));
-                }
-            }
-            */
-        }
-        if cands.len() > ntier2 {
-            cands.sort_unstable();
-            for cid in cands
-                .iter() // .skip(ntier1)
-                .skip(ntier2)
-            {
-                let c = &mut clause[cid.to()];
-                let cid = ClauseId::from(cid.to());
-                remove_clause_fn(
-                    certification_store,
-                    binary_link,
-                    watch_cache,
-                    num_bi_clause,
-                    num_clause,
-                    num_learnt,
-                    cid,
-                    c,
-                );
-                freelist.push(cid);
-            }
-        } else {
-            ntier2 = cands.len();
         }
-        self.last_reduction_at = num_conflict;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
     }

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);
+    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.