Splr-0.17.0 (#185)

- fix #188 - feature 'reward_annealing' #187 - `Certificate` handles empty clauses correctly #191 - fix stage calculations #194 - a better clause reduction #195 - SolverError::OutOfRange -> SolverError::InvalidLiteral #198 - SLS #159 #192 #199 - fix a build error without feature 'trail_saving' #202 - fix a build error without feature 'rephase' #205 - two-mode reduction (#208)
shnarazk · Jan 30, 2023 · 89ce01a · 89ce01a
1 parent bf2f324
commit 89ce01a
Show file tree

Hide file tree

Showing 31 changed files with 1,062 additions and 460 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.16.3"
+version = "0.17.0"
 authors = ["Narazaki Shuji <shujinarazaki@protonmail.com>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -11,53 +11,74 @@ homepage = "https://github.com/shnarazk/splr"
 keywords = ["SAT", "SAT-solver", "logic", "satisfiability"]
 categories = ["science", "mathematics"]
 default-run = "splr"
+rust-version = "1.65"
 
 [dependencies]
 bitflags = "^1.3"
 
 [features]
 default = [
-        # "boundary_check", # for DEBUG
-        # "bi_clause_completion", # increase memory pressure
-        # "no_clause_elimination",
+        ### Essential
+        # "incremental_solver",
+        "unsafe_access",
+
+        ### Heuristics
+        # "bi_clause_completion",
         # "clause_rewarding",
-        "clause_vivification",
         "dynamic_restart_threshold",
-        # "incremental_solver",
         "LRB_rewarding",
-        # "maintain_watch_cache", # for DEBUG
         "reason_side_rewarding",
         "rephase",
+        "reward_annealing",
+        # "stochastic_local_search",
         # "suppress_reason_chain",
+        "two_mode_reduction",
         "trail_saving",
-        "unsafe_access"
+
+        ### Logic formula processor
+        # "no_clause_elimination",
+        "clause_vivification",
+
+        ### For DEBUG
+        # "boundary_check",
+        # "maintain_watch_cache",
+        ]
+assign_rate = []                # for debug and study
+best_phases_tracking = []       # save the best-so-far assignment, used by 'rephase'
+bi_clause_completion = []       # this will increase memory pressure
+boundary_check = []             # for debug
+chrono_BT = []                  # NOT WORK
+no_clause_elimination = []      # pre(in)-processor setting
+clause_rewarding = []           # clauses have activities w/ decay rate
+clause_vivification = []        # pre(in)-processor setting
+debug_propagation = []          # for debug
+dynamic_restart_threshold = []  # control restart spans like Glucose
+EMA_calibration = []            # each exponential moving average has a calbration value
+EVSIDS = []                     # Eponential Variable State Independent Decaying Sum
+incremental_solver = [          # for all solution SAT sover
+        "no_clause_elimination",
+        ]
+just_used = []                  # Var and clause have 'just_used' flags
+LRB_rewarding = []              # Vearning Rate Based rewarding, a new var activity criteria
+maintain_watch_cache = []       # for DEBUG
+no_IO = []                      # to embed Splr into non-std environments
+reason_side_rewarding = []      # an idea used in Learning-rate based rewarding
+rephase = [                     # search around the best-so-far candidate repeatedly
+        "best_phases_tracking",
+        ]
+reward_annealing = []           # use bigger and smaller decay rates cycliclly
+stochastic_local_search = [     # since 0.17
+        # "reward_annealing",
+        "rephase",
         ]
-assign_rate = []
-best_phases_tracking = []
-bi_clause_completion = []
-boundary_check = []
-chrono_BT = []
-no_clause_elimination = []
-clause_rewarding = []
-clause_vivification = []
-debug_propagation = []
-dynamic_restart_threshold = []
-EMA_calibration = []
-EVSIDS = []
-incremental_solver = ["no_clause_elimination"]
-just_used = []
-LRB_rewarding = []
-maintain_watch_cache = []
-no_IO = []
-reason_side_rewarding = []
-rephase = ["best_phases_tracking"]
-support_user_assumption = []
-suppress_reason_chain = []
-trace_analysis = []
-trace_elimination = []
-trace_equivalency = []
-trail_saving = []
-unsafe_access = []
+support_user_assumption = []    # NOT WORK (defined in Glucose)
+suppress_reason_chain = []      # make direct links between a dicision var and its implications
+trace_analysis = []             # for debug
+trace_elimination = []          # for debug
+trace_equivalency = []          # for debug
+trail_saving = []               # reduce propagation cost by reusing propagation chain
+two_mode_reduction = []         # exploration mode and exploitation mode since 0.17
+unsafe_access = []              # access elements of vectors without boundary checking
 
 [profile.release]
 lto = "fat"

diff --git a/ChangeLog.md b/ChangeLog.md
@@ -1,3 +1,16 @@
+## 0.17.0, 2023-01-30
+
+- (Breaking change) `Certificate::try_from` returns `Ok` values even if a given vector
+  contains empty clauses. All expressions corresponding to valid CNFs should be
+  converted to `Certificate` successfully. On the other hand, `Solver::try_from` still
+  returns `SolverError::EmptyClause`. (#191, #196, #197)
+- Add a new feature 'reward_annealing' (#187)
+- Fix misc wrong calculations on Luby series and stage-cycle-segment model (#194)
+- Fix build errors without feature 'trial_saving' or 'rephase' (#202, #205)
+- clause reduction uses revised parameters matching a Luby series based parameter shifting
+  model (#195)
+- add feature 'two_mode_reduction'
+
 ## 0.16.3, 2022-09-16
 
 - Fix another bug on `add_var` and `add_assignment` (#183)

diff --git a/README.md b/README.md
@@ -21,11 +21,11 @@ Please check [ChangeLog](ChangeLog.md) about recent updates.
 
 Though Splr comes with **ABSOLUTELY NO WARRANTY**, I'd like to show some results.
 
-#### Version 0.15.0
+#### Version 0.17.0
 
-- [SAT Competition 2021](https://satcompetition.github.io/2021/), [Benchmarks main truck](https://satcompetition.github.io/2021/benchmarks.html) -- splr-0.15.0 solved with a 300 sec timeout:
-  - 42 satisfiable problems: all the solutions were correct.
-  - 34 unsatisfiable problems: all the certifications were verified with [Grat toolchain](https://www21.in.tum.de/~lammich/grat/).
+- [SAT Competition 2021](https://satcompetition.github.io/2021/), [Benchmarks main track](https://satcompetition.github.io/2021/benchmarks.html) -- splr-0.17.0 solved with a 300 sec timeout (this is one of the best of splr):
+  - 49 satisfiable problems: all the solutions were correct.
+  - 34 unsatisfiable problems: all certifications were verified with [Grat toolchain](https://www21.in.tum.de/~lammich/grat/) or [drat-trim](https://github.com/marijnheule/drat-trim).
 
 ## Install
 
@@ -137,7 +137,7 @@ unif-k3-r4.25-v360-c1530-S1028159446-096.cnf       360,1530 |time:   204.09
 s UNSATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
 ```
 
-#### A: Verify with drat-trim
+#### A: Verify with [drat-trim](https://github.com/marijnheule/drat-trim)
 
 ```plain
 $ drat-trim cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat
@@ -283,6 +283,29 @@ for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() {
 }
 ```
 
+#### sample code from my [sudoku solver](https://github.com/shnarazk/sudoku_sat/)
+
+https://github.com/shnarazk/sudoku_sat/blob/4490b4358e5f3b72803a566323a6c8c196627f92/src/bin/sudoku400.rs#L36-L60
+
+```rust
+    let mut solver = Solver::try_from((config, rules.as_ref())).expect("panic");
+    for a in setting.iter() {
+        solver.add_assignment(*a).expect("panic");
+    }
+    for ans in solver.iter().take(1) {
+        let mut picked = ans.iter().filter(|l| 0 < **l).collect::<Vec<&i32>>();
+        for _i in 1..=range {
+            for _j in 1..=range {
+                let (_i, _j, d, _b) = Cell::decode(*picked.remove(0));
+                print!("{:>2} ", d);
+            }
+            println!();
+        }
+        println!();
+    }
+}
+```
+
 ### Mnemonics used in the progress message
 
 | mnemonic     | meaning                                                                                   |
@@ -319,7 +342,7 @@ for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() {
 
 ```plain
 A modern CDCL SAT solver in Rust
-Activated features: best phase tracking, stage-based clause elimination, stage-based clause vivification, stage-based dynamic restart threshold, Learning-Rate Based rewarding, reason-side rewarding, stage-based re-phasing, trail saving, unsafe access
+Activated features: best phase tracking, stage-based clause elimination, stage-based clause vivification, stage-based dynamic restart threshold, Learning-Rate Based rewarding, reason-side rewarding, stage-based re-phasing, two-mode reduction, trail saving, unsafe access
 
 USAGE:
   splr [FLAGS] [OPTIONS] <cnf-file>
@@ -333,21 +356,24 @@ FLAGS:
   -V, --version             Prints version information
 OPTIONS:
       --cl <c-cls-lim>      Soft limit of #clauses (6MC/GB)         0
-  -t, --timeout <timeout>   CPU time limit in sec.               5000
+      --crl <cls-rdc-lbd>   Clause reduction LBD threshold          5
+      --cr1 <cls-rdc-rm1>   Clause reduction ratio for mode1        0.20
+      --cr2 <cls-rdc-rm2>   Clause reduction ratio for mode2        0.05
       --ecl <elm-cls-lim>   Max #lit for clause subsume            64
       --evl <elm-grw-lim>   Grow limit of #cls in var elim.         0
       --evo <elm-var-occ>   Max #cls for var elimination        20000
   -o, --dir <io-outdir>     Output directory                         .
   -p, --proof <io-pfile>    DRAT Cert. filename                 proof.drat
   -r, --result <io-rfile>   Result filename/stdout
+  -t, --timeout <timeout>   CPU time limit in sec.               5000
       --vdr <vrw-dcy-rat>   Var reward decay rate                   0.96
 ARGS:
   <cnf-file>    DIMACS CNF file
 ```
 
 ## Solver description
 
-Splr-0.15.0 adopts the following features by default:
+Splr-0.17.0 adopts the following features by default:
 
 - Learning-rate based (LRB) var rewarding and clause rewarding[4]
 - Reason-side var rewarding[4]
@@ -360,12 +386,13 @@ Splr-0.15.0 adopts the following features by default:
   - re-configuration of var phases and var activities
   - re-configuration of trail saving extended with reason refinement based on clause quality[3].
 
-Splr-0.15.0 discarded various dynamic and heuristic-based control schemes used in 0.14.0.
-The following figure shows the details.
+(Splr-0.15.0 and upper try to discard various dynamic and heuristic-based control schemes used in the previous versions.)
+
+The following figure explains the flow used in the latest Splr.
 
-![search algorithm in Splr 0.14](https://user-images.githubusercontent.com/997855/161426178-8264d3e2-e68a-4d64-86b4-906155a51039.png)
+![search algorithm in Splr 0.17](https://user-images.githubusercontent.com/997855/215309646-1bfe3ea5-dcc3-42ee-9d76-99e1b07610c4.png)
 
-Note: I use the following terms here:
+I use the following terms here:
 - _a stage_ -- a span in which solver uses the same restart parameters
 - _a cycle_ -- a group of continuos spans of which the corresponding Luby values make a non-decreasing sequence
 - _a segment_ -- a group of continuos cycles which are separated by new maximum Luby values' occurrences

diff --git a/cnfs/README.md b/cnfs/README.md
@@ -0,0 +1,32 @@
+# A sample CNF collection
+
+### Corner cases
+
+If you try to build your SAT solver from scratch, they are corner cases you have to pay attention.
+
+- [empty-clause.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/empty-clause.cnf)
+- [empty-form.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/empty-form.cnf)
+
+### Basic examples
+
+If you think to complete CDCL algorithm, check with them.
+
+- [sample.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/sample.cnf)
+- [unsat.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unsat.cnf)
+- [uf8.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf8.cnf)
+- [uf20-01.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf20-01.cnf)
+
+### Midde scale problems
+
+And you think your solver is great, try them. 3-SAT problems (N=360) are hard. But your solver must solve them.
+
+- [uf100-010.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf100-010.cnf)
+- [uf250-02.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf250-02.cnf)
+- [unif-k3-r4.25-v360-c1530-S1028159446-096.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf)
+- [unif-k3-r4.25-v360-c1530-S1293537826-039.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf)
+
+### Problems from the real competition
+
+If you catched up the implementations of modern solvers and reasech trend, try it.
+
+- [a_rphp035_05.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/a_rphp035_05.cnf)
diff --git a/flake.nix b/flake.nix
@@ -14,7 +14,7 @@
                 stdenv.mkDerivation rec {
                   name = "splr-${version}";
                   pname = "splr";
-                  version = "0.16.3-20220916";
+                  version = "0.17.0-20230129";
                   src = self;
                   buildInputs = [ cargo libiconv rustc binutils ];
                   buildPhase = "cargo build --release";

diff --git a/misc/algorithm.tex b/misc/algorithm.tex
@@ -24,19 +24,19 @@
     \If{a new stage begins}{
         REDUCE()\;
         update restart conditions\;
-    }
-    \If{a new cycle begins}{
-        VIVIFY()\;
-        select var phases\;
-    }
-    \If{a new segment begins}{
-        ELIMINATE()\;
-        rescale var activities\;
+        \If{a new cycle begins}{
+            VIVIFY()\;
+            select var phases\;
+            \If{a new segment begins}{
+                ELIMINATE()\;
+                rescale var activities\;
+            }
+        }
     }
   }
 }
 \Return{SAT}\;
 }
-\caption{Main search loop in Splr-0.15 (src/solver/search.rs)}
+\caption{Main search loop in Splr-0.17 (src/solver/search.rs)}
 \end{algorithm}
 \end{document}
diff --git a/src/assign/evsids.rs b/src/assign/evsids.rs
@@ -29,6 +29,12 @@ impl ActivityIF<VarId> for AssignStack {
             self.activity_decay_step *= SCALE;
         }
     }
+    fn update_activity_decay(&mut self, _: f64) {
+        self.activity_decay = self
+            .activity_decay_default
+            .min(self.activity_decay + self.activity_decay_step);
+        self.activity_anti_decay = 1.0 - self.activity_decay;
+    }
     fn update_activity_tick(&mut self) {
         const INC_SCALE: f64 = 1.01;
         if self.ordinal == 0 {
@@ -38,10 +44,4 @@ impl ActivityIF<VarId> for AssignStack {
         self.ordinal += 1;
         self.activity_decay_step *= INC_SCALE;
     }
-    fn update_activity_decay(&mut self, _index: Option<usize>) {
-        self.activity_decay = self
-            .activity_decay_default
-            .min(self.activity_decay + self.activity_decay_step);
-        self.activity_anti_decay = 1.0 - self.activity_decay;
-    }
 }
diff --git a/src/assign/heap.rs b/src/assign/heap.rs
@@ -1,9 +1,10 @@
+///
 /// Heap struct for selecting decision vars
-use {
-    super::{AssignStack, TrailSavingIF},
-    crate::types::*,
-    std::fmt,
-};
+///
+use {super::AssignStack, crate::types::*, std::fmt};
+
+#[cfg(feature = "trail_saving")]
+use super::TrailSavingIF;
 
 /// Heap of VarId, based on var activity.
 // # Note
@@ -187,8 +188,8 @@ impl VarOrderIF for VarIdHeap {
         let vs = self.heap[s];
         let n = self.idxs[0];
         let vn = self.heap[n as usize];
-        debug_assert!(vn != 0, "Invalid VarId for heap: vn {}, n {}", vn, n);
-        debug_assert!(vs != 0, "Invalid VarId for heap: vs {}, n {}", vs, n);
+        debug_assert!(vn != 0, "Invalid VarId for heap: vn {vn}, n {n}");
+        debug_assert!(vs != 0, "Invalid VarId for heap: vs {vs}, n {n}");
         self.heap.swap(n as usize, s);
         self.idxs.swap(vn as usize, vs as usize);
         self.idxs[0] -= 1;
@@ -197,6 +198,7 @@ impl VarOrderIF for VarIdHeap {
     fn len(&self) -> usize {
         self.idxs[0] as usize
     }
+    #[allow(clippy::unnecessary_cast)]
     fn insert(&mut self, vi: VarId) -> usize {
         if self.contains(vi) {
             return self.idxs[vi as usize] as usize;
@@ -249,6 +251,6 @@ impl VarIdHeap {
                 panic!("idxs {} {} {:?}", i, d[i], d);
             }
         }
-        println!(" - pass var_order test at {}", s);
+        println!(" - pass var_order test at {s}");
     }
 }