dev-0.19.0

.envrc

@@ -0,0 +1,3 @@
+# shellcheck shell=bash
+source $HOME/.config/direnv/envrc
+use flake

.github/dependabot.yml

@@ -8,4 +8,8 @@ updates:
   - package-ecosystem: "cargo" # See documentation for possible values
     directory: "/" # Location of package manifests
     schedule:
-      interval: "daily"
+      interval: "weekly"
+  - package-ecosystem: "nix" # See documentation for possible values
+    directory: "/" # Location of package manifests
+    schedule:
+      interval: "weekly"

.gitignore

@@ -8,9 +8,10 @@
 # These are backup files generated by rustfmt
 **/*.rs.bk
 
-*.cnf
+*.cnf*
 .ans_*
 .vscode
 *.ipynb
 /result
 .cargo
+proof.drat

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.18.0"
+version = "0.19.0-rc5"
 authors = ["Narazaki Shuji <shujinarazaki@protonmail.com>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2024"
@@ -11,7 +11,7 @@ homepage = "https://github.com/shnarazk/splr"
 keywords = ["SAT", "SAT-solver", "logic", "satisfiability"]
 categories = ["science", "mathematics"]
 default-run = "splr"
-rust-version = "1.94"
+rust-version = "1.95"
 
 [dependencies]
 bitflags = "^2.8"
@@ -23,67 +23,40 @@ default = [
     "unsafe_access",
     # "chrono_BT",
     "trail_saving",
-    "BT_deepen",
+    # "BT_deepen",
 
     ### Heuristics
-    # "bi_clause_completion",
-    # "clause_rewarding",
-    "dynamic_restart_threshold",
-    "LRB_rewarding",
     "reason_side_rewarding",
     "rephase",
-    "reward_annealing",
     # "stochastic_local_search",
-    # "suppress_reason_chain",
-    "two_mode_reduction",
 
     ### Logic formula processor
     "clause_elimination",
     "clause_vivification",
 
-    ### For DEBUG
-    # "boundary_check",
-    # "maintain_watch_cache",
-
     ### platform dependency
     # "platform_wasm"
 ]
-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
+
 BT_deepen = []                   # backtrack drift
 chrono_BT = []                  # NOT WORK
 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 = []                     # Exponential Variable State Independent Decaying Sum
-just_used = []                  # Var and clause have 'just_used' flags
-LRB_rewarding = []              # Learning Rate Based rewarding, a new var activity criteria
-maintain_watch_cache = []       # for DEBUG
 no_IO = []                      # to embed Splr into non-std environments
 platform_wasm = [
     "instant",                  # use instant::Duration instead of std::time::Duration
 ]
 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",
-]
-support_user_assumption = []    # NOT WORK (defined in Glucose)
-suppress_reason_chain = []      # make direct links between a dicision var and its implications
+rephase = []                    # search around the best-so-far candidate repeatedly
+# stochastic_local_search = [     # since 0.17
+#     "rephase",
+# ]
+
 trace_analysis = []             # for debug
 trace_elimination = []          # for debug
-trace_equivalency = []          # for debug
+trace_propagation = []          # 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]

ChangeLog.md

@@ -1,3 +1,28 @@
+## 0.19.0, 2026-0X-XX
+
+- Adopt decision literal select heuristics:
+    - *Variable Move To queue First*
+    - *LearningRate-Based Rewarding* 
+- Adopt rephasing modes: Walk, Best, False(Original), True(Inverted), Random, Flipped
+- Revise `ClauseDB::reduce` to remove much more clauses
+- Switch to the O(1) Luby iterator. Now Luby sequence is used for
+  - trigger for restarts, clause elimination, and clause vivification
+  - clause DB size after clause reduction
+- `ClauseDBIF::reduce` can run at any decision level, and runs every 40,000 conflicts
+- Remove feature 'assign_rate'
+- Remove feature 'bi_clause_completion'
+- Remove feature 'boundary_check'
+- Remove feature 'dynamic_restart_threshold'
+- Remove feature 'EVSIDS'
+- Remove feature 'just_used'
+- Remove feature 'maintain_watch_cache'
+- Remove feature 'reward_annealing'
+- Remove feature 'suppress_reason_chain'
+- Remove feature 'trace_equivalency'
+- Remove feature 'two_mode_reduction'
+- rename feature 'debug_propagation' to 'trace_propagation'
+- Remove src/solver/restart.rs
+
 ## 0.18.0, 2026-03-14
 
 This would be no better than the previous implementations.

README.md

@@ -1,15 +1,14 @@
 ## A modern SAT Solver for Propositional Logic in Rust
 
-Splr is a modern SAT solver in [Rust](https://www.rust-lang.org), based on [Glucose 4.1](https://www.labri.fr/perso/lsimon/glucose/).
+Splr is a modern SAT solver in [Rust](https://www.rust-lang.org), based on [Glucose 4.1](https://www.labri.fr/perso/lsimon/glucose/), inspired by [Kissat](https://github.com/arminbiere/kissat).
 It adopts, or adopted, various research results on modern SAT solvers:
 
-- _CDCL_, _watch literals_, _LBD_ and so on from Glucose, [Minisat](http://minisat.se) and the ancestors
-- Luby series based restart control
+- _CDCL_, _watch literals_, _LBD_ and so on from Kissat, Glucose, [Minisat](http://minisat.se) and the ancestors
+- Luby series based restart control. The current implementation has $O(1)$ time complexity and $O(1)$ space complexity.
 - Glucose-like _dynamic blocking/forcing restarts_
 - pre/in-processor to simplify the given CNF
-- branching variable selection based on _Learning Rate Based Branching_ with _Reason Side Rewarding_ or EVSIDS
-- [CaDiCaL](https://github.com/arminbiere/cadical)-like extended phase saving
-- _restart stabilization_ inspired by CadiCaL
+- branching variable selections based on _Learning Rate Based Branching_ with _Reason Side Rewarding_ or EVSIDS and _Variable Move To the quest First_, VMTF
+- Kissat-like various rephasing scheme rotation
 - _clause vivification_
 - _trail saving_