20240323 rayon propagate

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.17.0"
+version = "0.18.0-alpha.2"
 authors = ["Narazaki Shuji <[email protected]>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -14,7 +14,8 @@ default-run = "splr"
 rust-version = "1.65"
 
 [dependencies]
-bitflags = "^1.3"
+bitflags = "^2.1"
+rayon = "^1.7"
 
 [features]
 default = [

README.md

@@ -419,4 +419,4 @@ file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 ---
 
-2020-2022, Narazaki Shuji
+2020-2023, Narazaki Shuji

src/cdb/db.rs

@@ -227,18 +227,40 @@ impl ClauseDBIF for ClauseDB {
         self.binary_link.connect_with(l)
     }
     // watch_cache_IF
+    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, &Vec<Lit>, Lit)> {
+        if len == 0 {
+            self.watch_cache[lit]
+                .iter()
+                .skip(start)
+                .map(|(cid, l)| (*cid, &self[*cid].lits, *l))
+                .collect::<Vec<_>>()
+        } else {
+            self.watch_cache[lit]
+                .iter()
+                .skip(start)
+                .take(len)
+                .map(|(cid, l)| (*cid, &self[*cid].lits, *l))
+                .collect::<Vec<_>>()
+        }
+    }
+    fn watcher_list_swap(&mut self, lit: Lit, index_a: usize, index_b: usize) {
+        self.watch_cache[lit].swap(index_a, index_b);
+    }
+    fn watcher_list_len(&self, lit: Lit) -> usize {
+        self.watch_cache[lit].len()
+    }
     fn fetch_watch_cache_entry(&self, lit: Lit, wix: WatchCacheProxy) -> (ClauseId, Lit) {
         self.watch_cache[lit][wix]
     }
     #[inline]
-    fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator {
+    fn watch_cache_iter(&mut self, lit: Lit) -> WatchCacheIterator {
         // let mut empty = WatchCache::new();
-        // std::mem::swap(&mut self.watch_cache[l], &mut empty);
+        // std::mem::swap(&mut self.watch_cache[lit], &mut empty);
         // empty
-        WatchCacheIterator::new(self.watch_cache[l].len())
+        WatchCacheIterator::new(self.watch_cache[lit].len())
     }
-    fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator) {
-        self.watch_cache[l].swap_remove(iter.index);
+    fn detach_watch_cache(&mut self, lit: Lit, iter: &mut WatchCacheIterator) {
+        self.watch_cache[lit].swap_remove(iter.index);
         iter.detach_entry();
     }
     fn merge_watch_cache(&mut self, p: Lit, wc: WatchCache) {
@@ -483,6 +505,125 @@ impl ClauseDBIF for ClauseDB {
 
         iter.restore_entry();
     }
+    fn transform2_by_updating_watch_cache(
+        &mut self,
+        propagating_lit: Lit,
+        cid: ClauseId,
+        old_watch_index: usize,
+        new_watch_index: usize,
+    ) {
+        //
+        //## Clause transform rules
+        //
+        // There is one case under non maintain_blocker:
+        // 1. one deletion (if not removed), and one insertion of watch caches
+        //
+        // There is one case under maintain_blocker:
+        // 1. one deletion (if not removed), one insertion, and one update
+        //
+        // So the proceduce is
+        // 1. delete an old one                   [Step:1]
+        // 2. insert a new watch                  [Step:2]
+        // 3. update a blocker cach e             [Step:3]
+
+        debug_assert!(!self[cid].is_dead());
+        debug_assert!(old_watch_index < 2);
+        debug_assert!(1 < new_watch_index);
+        let ClauseDB {
+            ref mut clause,
+            ref mut watch_cache,
+            ..
+        } = self;
+        let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
+        let another_watch = c.lits[(old_watch_index == 0) as usize];
+
+        //## Step:1 detaching this clause from old wathes's list.
+        // But `transform2_by_resizing_watch_list` will clear it. So nothing needed here.
+        debug_assert_eq!(propagating_lit, !c.lits[old_watch_index]);
+
+        //## Step:2
+        // assert!(watch_cache[!c.lits[new]].iter().all(|e| e.0 != cid));
+        watch_cache[!c.lits[new_watch_index]].insert_watch(cid, another_watch);
+
+        #[cfg(feature = "maintain_watch_cache")]
+        {
+            //## Step:3
+            watch_cache[!c.lits[another_watch]].update_watch(cid, c.lits[new_watch_index]);
+        }
+
+        c.lits.swap(old_watch_index, new_watch_index);
+        c.search_from = (new_watch_index + 1) as u16;
+        // maintain_watch_literal \\ assert!(watch_cache[!c.lits[0]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[1]));
+        // maintain_watch_literal \\ assert!(watch_cache[!c.lits[1]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[0]));
+    }
+    fn transform2_by_pushing_watch_cache_back(
+        &mut self,
+        l: Lit,
+        from: usize,
+        to: &mut usize,
+        op: Option<Lit>,
+    ) {
+        if let Some(p) = op {
+            assert_ne!(p, l);
+            self.watch_cache[l][from].1 = p;
+        }
+        self.watch_cache[l][*to] = self.watch_cache[l][from];
+
+        {
+            // self.watch_cache[l][from].0 = ClauseId::default();
+            let cid = self.watch_cache[l][*to].0;
+            let c = &self[cid];
+            let l0 = c.lits[0];
+            let l1 = c.lits[1];
+            debug_assert!(self.watch_cache[!l0]
+                .iter()
+                .any(|wc| wc.0 == cid && wc.1 != l0));
+            debug_assert!(self.watch_cache[!l1]
+                .iter()
+                .any(|wc| wc.0 == cid && wc.1 != l1));
+            // if !(self.watch_cache[!l0]
+            //     .iter()
+            //     .any(|wc| wc.0 == cid && wc.1 == l1))
+            // {
+            //     println!(
+            //         "{cid}: {c:?}, {l0}, {l1}, propagating: {l}, watch on !{l0} contains {:?}, op: {op:?}",
+            //         self.watch_cache[!l0]
+            //             .iter()
+            //             .filter(|wc| wc.0 == cid)
+            //             .collect::<Vec<_>>(),
+            //     );
+            //     // panic!();
+            // }
+            // assert!(self.watch_cache[!l0]
+            //     .iter()
+            //     .any(|wc| wc.0 == cid && wc.1 == l1));
+            // assert!(self.watch_cache[!l1]
+            //     .iter()
+            //     .any(|wc| wc.0 == cid && wc.1 == l0));
+        }
+        *to += 1;
+    }
+    fn transform2_by_resizing_watch_cache_list(&mut self, l: Lit, to: usize) {
+        debug_assert!(to <= self.watch_cache[l].len());
+        self.watch_cache[l].truncate(to);
+    }
+    fn transform2_by_folding_watch_cache_list(
+        &mut self,
+        propagating: Lit,
+        garbage_from: usize,
+        remain_from: usize,
+    ) {
+        let watcher = &mut self.watch_cache[propagating];
+        let len = watcher.len();
+        let mut last = garbage_from;
+        for i in remain_from..len {
+            watcher[last] = watcher[i];
+            last += 1;
+        }
+        assert!(last <= len);
+        watcher.truncate(last);
+    }
+
     // return a Lit if the clause becomes a unit clause.
     fn transform_by_elimination(&mut self, cid: ClauseId, p: Lit) -> RefClause {
         //
@@ -922,7 +1063,7 @@ impl ClauseDBIF for ClauseDB {
         }
 
         c.lits.swap(old, new);
-
+        c.search_from = (new + 1) as u16;
         // maintain_watch_literal \\ assert!(watch_cache[!c.lits[0]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[1]));
         // maintain_watch_literal \\ assert!(watch_cache[!c.lits[1]].iter().any(|wc| wc.0 == cid && wc.1 == c.lits[0]));
     }
@@ -1204,7 +1345,9 @@ impl ClauseDBIF for ClauseDB {
                 panic!("conflicting var {} {:?}", vi, asg.assign(vi));
             }
         }
-        let Ok(out) = File::create(fname) else { return; };
+        let Ok(out) = File::create(fname) else {
+            return;
+        };
         let mut buf = std::io::BufWriter::new(out);
         let na = asg.derefer(crate::assign::property::Tusize::NumAssertedVar);
         let nc = self.iter().skip(1).filter(|c| !c.is_dead()).count();

src/cdb/mod.rs

@@ -95,14 +95,18 @@ pub trait ClauseDBIF:
     //## abstraction to watch_cache
     //
 
+    // return the number of clause watching `lit`
+    fn watcher_list(&self, lit: Lit, start: usize, len: usize) -> Vec<(ClauseId, &Vec<Lit>, Lit)>;
+    fn watcher_list_swap(&mut self, lit: Lit, index_a: usize, index_b: usize);
+    fn watcher_list_len(&self, lit: Lit) -> usize;
     // get mutable reference to a watch_cache
     fn fetch_watch_cache_entry(&self, lit: Lit, index: WatchCacheProxy) -> (ClauseId, Lit);
     /// replace the mutable watcher list with an empty one, and return the list
-    fn watch_cache_iter(&mut self, l: Lit) -> WatchCacheIterator;
+    fn watch_cache_iter(&mut self, lit: Lit) -> WatchCacheIterator;
     /// detach the watch_cache referred by the head of a watch_cache iterator
-    fn detach_watch_cache(&mut self, l: Lit, iter: &mut WatchCacheIterator);
+    fn detach_watch_cache(&mut self, lit: Lit, iter: &mut WatchCacheIterator);
     /// Merge two watch cache
-    fn merge_watch_cache(&mut self, l: Lit, wc: WatchCache);
+    fn merge_watch_cache(&mut self, lit: Lit, wc: WatchCache);
     /// swap the first two literals in a clause.
     fn swap_watch(&mut self, cid: ClauseId);
 
@@ -117,6 +121,32 @@ pub trait ClauseDBIF:
         iter: &mut WatchCacheIterator,
         p: Option<Lit>,
     );
+    /// FIXME:
+    fn transform2_by_updating_watch_cache(
+        &mut self,
+        propagating_lit: Lit,
+        cid: ClauseId,
+        old_watch_index: usize,
+        new_watch_index: usize,
+    );
+    /// FIXME: rayon_propagate
+    fn transform2_by_pushing_watch_cache_back(
+        &mut self,
+        l: Lit,
+        from: usize,
+        to: &mut usize,
+        op: Option<Lit>,
+    );
+    /// FIXME:
+    fn transform2_by_resizing_watch_cache_list(&mut self, l: Lit, to: usize);
+    /// FIXME:
+    fn transform2_by_folding_watch_cache_list(
+        &mut self,
+        propagating: Lit,
+        garbage_from: usize,
+        remain_from: usize,
+    );
+
     /// swap i-th watch with j-th literal then update watch caches correctly
     fn transform_by_updating_watch(&mut self, cid: ClauseId, old: usize, new: usize, removed: bool);
     /// allocate a new clause and return its id.

src/cdb/watch_cache.rs

@@ -96,6 +96,7 @@ impl IndexMut<Lit> for Vec<WatchCache> {
 
 pub type WatchCacheProxy = usize;
 
+#[derive(Clone, Debug)]
 pub struct WatchCacheIterator {
     pub index: usize,
     end_at: usize,
@@ -109,7 +110,9 @@ impl Iterator for WatchCacheIterator {
         (self.index < self.end_at).then_some({
             // assert!(0 < self.checksum);
             // self.checksum -= 1;
-            self.index
+            let current = self.index;
+            self.index += 1;
+            current
         })
     }
 }
@@ -122,6 +125,17 @@ impl WatchCacheIterator {
             // checksum: len,
         }
     }
+    pub fn skip(mut self, start: usize) -> Self {
+        self.index = start;
+        self
+    }
+    pub fn take(mut self, count: usize) -> Self {
+        self.end_at = self.end_at.min(self.index + count);
+        self
+    }
+    pub fn current(&mut self) -> Option<WatchCacheProxy> {
+        (self.index < self.end_at).then_some(self.index)
+    }
     pub fn restore_entry(&mut self) {
         self.index += 1;
     }

src/types.rs

@@ -398,22 +398,17 @@ impl fmt::Display for SolverError {
 pub type MaybeInconsistent = Result<(), SolverError>;
 
 /// CNF locator
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Default)]
 pub enum CNFIndicator {
     /// not specified
+    #[default]
     Void,
     /// from a file
     File(String),
     /// embedded directly
     LitVec(usize),
 }
 
-impl Default for CNFIndicator {
-    fn default() -> Self {
-        CNFIndicator::Void
-    }
-}
-
 impl fmt::Display for CNFIndicator {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match self {
@@ -570,6 +565,7 @@ pub trait FlagIF {
 
 bitflags! {
     /// Misc flags used by [`Clause`](`crate::cdb::Clause`).
+    #[derive(Clone, 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;
@@ -586,6 +582,7 @@ bitflags! {
 
 bitflags! {
     /// Misc flags used by [`Var`](`crate::assign::Var`).
+    #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
     pub struct FlagVar: u8 {
         /// * the previous assigned value of a Var.
         const PHASE        = 0b0000_0001;