Lib.rs

Rust 中命题逻辑的现代 SAT 求解器

Splr 是基于 Rust 的现代 SAT 求解器，基于 Glucose 4.1。它采用了或采用了现代 SAT 求解器的各种研究成果

• 从 Glucose、Minisat 及其祖先中获得的 CDCL、watch literals、LBD 等
• 基于 Luby 系列的重启控制
• 类似 Glucose 的 动态阻塞/强制重启
• 简化给定的 CNF 的前/处理
• 基于 基于学习率分支 的分支变量选择，带有 Reason Side Rewarding 或 EVSIDS
• CaDiCaL 类的扩展阶段保存
• 受到 CadiCaL 启发的 重启稳定化
• 子句活化
• 跟踪保存

感谢 SAT 研究人员。

请查看关于最近更新的 变更日志。

正确性

虽然 Splr 附带 绝对没有任何保证，但我愿意展示一些结果。

版本 0.17.0

• SAT 竞赛 2021，基准测试主赛道 -- splr-0.17.0 在 300 秒超时内解决（这是 splr 中的最佳之一）
  • 49 个可满足问题：所有解决方案都是正确的。
  • 34 个不可满足问题：所有证书都通过 Grat 工具链 或 drat-trim 进行了验证。

安装

安装最新版本的 cargo 后，只需运行 cargo install splr。将安装两个可执行文件

• splr -- 求解器
• dmcr -- 一个非常简单的模型检查器，用于验证由 splr 生成的 可满足 赋值集。

或者，Nix 用户可以使用 nix build。

关于 no_std 环境和特性 no_IO

如果您想为 no_std 环境构建库，或者如果您想使用 no_IO 功能进行编译，您必须运行以下命令：cargo build --lib --features no_IO。它们与 cargo install 不兼容。

• [2024-02-03] 新增了功能 platform_wasm。

用法

Splr 是一个独立程序，接受一个 CNF 文件。结果将保存到文件中，其格式由 SAT 竞赛 2011 规则 定义。

$ splr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
unif-k3-r4.25-v360-c1530-S1293537826-039.cnf       360,1530 |time:   732.01
 #conflict:    9663289, #decision:     23326959, #propagate:      546184944
  Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000
      Clause|Remv:    69224, LBD2:     2857, BinC:        1, Perm:     1522
    Conflict|entg:   7.0499, cLvl:  12.2451, bLvl:  11.1030, /cpr:    30.74
    Learning|avrg:  10.4375, trnd:   1.0069, #RST:   566140, /dpc:     1.18
        misc|vivC:     7370, subC:        0, core:      122, /ppc:    61.53
      Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
s SATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf

$ cat ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
c This file was generated by splr-0.15.0 for cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
c
c unif-k3-r4.25-v360-c1530-S1293537826-039.cnf, #var:      360, #cls:     1530
c  #conflict:    9663289, #decision:     23326959, #propagate:      546184944,
c   Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000,
c       Clause|Remv:    69224, LBD2:     2857, BinC:        1, Perm:     1522,
c     Conflict|entg:   7.0499, cLvl:  12.2451, bLvl:  11.1030, /cpr:    30.74,
c      Learing|avrg:  10.4375, trnd:   1.0069, #RST:   566140, /dpc:     1.18,
c         misc|vivC:     7370, subC:        0, core:      122, /ppc:    61.53,
c     Strategy|mode:  generic, time:   732.03,
c
c   config::VarRewardDecayRate                       0.960
c   assign::NumConflict                        9663289
c   assign::NumDecision                       23326959
c   assign::NumPropagation                   546184944
c   assign::NumRephase                             734
c   assign::NumRestart                          566141
c   assign::NumVar                                 360
c   assign::NumAssertedVar                           0
c   assign::NumEliminatedVar                         9
c   assign::NumReconflict                          653
c   assign::NumRepropagation                  12460396
c   assign::NumUnassertedVar                       351
c   assign::NumUnassignedVar                       351
c   assign::NumUnreachableVar                        0
c   assign::RootLevel                                0
c   assign::AssignRate                               0.000
c   assign::DecisionPerConflict                      1.179
c   assign::PropagationPerConflict                  61.527
c   assign::ConflictPerRestart                     122.388
c   assign::ConflictPerBaseRestart                 122.388
c   assign::BestPhaseDivergenceRate                  0.000
c   clause::NumBiClause                              1
c   clause::NumBiClauseCompletion                    0
c   clause::NumBiLearnt                              1
c   clause::NumClause                            70746
c   clause::NumLBD2                               2857
c   clause::NumLearnt                            69224
c   clause::NumReduction                          1461
c   clause::NumReRegistration                        0
c   clause::Timestamp                                0
c   clause::LiteralBlockDistance                    10.438
c   clause::LiteralBlockEntanglement                 7.050
c   state::Vivification                            735
c   state::VivifiedClause                         7370
c   state::VivifiedVar                               0
c   state::NumCycle                                734
c   state::NumStage                               1461
c   state::IntervalScale                             1
c   state::IntervalScaleMax                       1024
c   state::BackjumpLevel                            11.103
c   state::ConflictLevel                            12.245
c
s SATISFIABLE
v 1 -2 3 4 5 6 -7 -8 9 -10 -11 -12 13 -14 ...  -360 0

$ dmcr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
A valid assignment set for cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf is found in ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf

如果您想证明不可满足性，请使用 --certify 或 -c，并使用如 Grid 这样的证明检查器。

首先使用证书选项 -c 运行 splr。

$ splr -c cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
unif-k3-r4.25-v360-c1530-S1028159446-096.cnf       360,1530 |time:   204.09
 #conflict:    4018458, #decision:      9511129, #propagate:      221662222
  Assignment|#rem:      345, #fix:        7, #elm:        8, prg%:   4.1667
      Clause|Remv:    11290, LBD2:     2018, BinC:      137, Perm:     1517
    Conflict|entg:   4.5352, cLvl:   8.0716, bLvl:   6.9145, /cpr:   112.08
    Learning|avrg:   1.5625, trnd:   0.2219, #RST:   237295, /dpc:     1.07
        misc|vivC:     4085, subC:        0, core:      345, /ppc:    52.55
      Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
 Certificate|file: proof.drat
s UNSATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf

A: 使用 drat-trim 验证

$ drat-trim cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat
c parsing input formula with 360 variables and 1530 clauses
c finished parsing
c detected empty clause; start verification via backward checking
c 1530 of 1530 clauses in core
c 2036187 of 4029964 lemmas in core using 68451907 resolution steps
c 0 RAT lemmas in core; 908116 redundant literals in core lemmas
s VERIFIED
c verification time: 105.841 seconds

B: 使用 gratchk 验证

首先，您必须将生成的 DRAT 文件转换为 GRAT 文件。

$ gratgen cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat -o proof.grat
c sizeof(cdb_t) = 4
c sizeof(cdb_t*) = 8
c Using RAT run heuristics
c Parsing formula ... 1ms
c Parsing proof (ASCII format) ... 32251ms
c Forward pass ... 2073ms
c Starting Backward pass
c Single threaded mode

0%   10   20   30   40   50   60   70   80   90   100%
|----|----|----|----|----|----|----|----|----|----|
***************************************************
c Waiting for aux-threads ...done
c Lemmas processed by threads: 2032698 mdev: 0
c Finished Backward pass: 65356ms
c Writing combined proof ... 19088ms
s VERIFIED
c Timing statistics (ms)
c Parsing:  32253
c Checking: 67465
c   * bwd:  65356
c Writing:  19088
c Overall:  118808
c   * vrf:  99720

c Lemma statistics
c RUP lemmas:  2032698
c RAT lemmas:  0
c   RAT run heuristics:   0
c Total lemmas:  2032698

c Size statistics (bytes)
c Number of clauses: 4031493
c Clause DB size:  309680252
c Item list:       128778112
c Pivots store:    16777216

然后使用 gratchk 验证它。

$ gratchk unsat cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.grat
c Reading cnf
c Reading proof
c Done
c Verifying unsat
s VERIFIED UNSAT

从 Rust 程序中调用 Splr

从 0.4.0 版本开始，您可以在您的程序中使用 Splr。（这里假设您使用 Rust 2021。）

use splr::*;

fn main() {
    let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]];
    match Certificate::try_from(v) {
        Ok(Certificate::SAT(ans)) => println!("s SATISFIABLE: {:?}", ans),
        Ok(Certificate::UNSAT) => println!("s UNSATISFIABLE"),
        Err(e) => panic!("s UNKNOWN; {}", e),
    }
}

所有解决方案 SAT 求解器都是作为 'incremental_solver' 功能的应用程序

以下示例需要 'incremental_solver' 功能。您需要以下依赖项

splr = { version = "^0.17", features = ["incremental_solver"] }

在此配置下，模块 splr 提供了一些额外的功能

• splr::求解器::重置(&mut self)
• splr::Solver::add_var(&mut self) // 增加最后一个变量的编号
• splr::求解器::添加子句(&mut self,vec: AsRef<[i32]>) -> Result<&mutSolver, SolverError>

在调用 add_var、add_clause 和 solve 之前，您必须先调用 reset。通过这种方式，splr 忘记了关于之前公式的所有信息，特别是由预处理器/中间处理器（如子句归约）引起的非等价变换。所以从技术上讲，splr 不是一个增量求解器。

如果 vec 无效，则 'add_clause' 将会发出错误。

use splr::*;
use std::env::args;

fn main() {
    let cnf = args().nth(1).expect("takes an arg");
    let assigns: Vec<i32> = Vec::new();
    println!("#solutions: {}", run(&cnf, &assigns));
}

#[cfg(feature = "incremental_solver")]
fn run(cnf: &str, assigns: &[i32]) -> usize {
    let mut solver = Solver::try_from(cnf).expect("panic at loading a CNF");
    for n in assigns.iter() {
        solver.add_assignment(*n).expect("panic at assertion");
    }
    let mut count = 0;
    loop {
        match solver.solve() {
            Ok(Certificate::SAT(ans)) => {
                count += 1;
                println!("s SATISFIABLE({}): {:?}", count, ans);
                let ans = ans.iter().map(|i| -i).collect::<Vec<i32>>();
                match solver.add_clause(ans) {
                    Err(SolverError::Inconsistent) => {
                        println!("c no answer due to level zero conflict");
                        break;
                    }
                    Err(e) => {
                        println!("s UNKNOWN; {:?}", e);
                        break;
                    }
                    Ok(_) => solver.reset(),
                }
            }
            Ok(Certificate::UNSAT) => {
                println!("s UNSATISFIABLE");
                break;
            }
            Err(e) => {
                println!("s UNKNOWN; {}", e);
                break;
            }
        }
    }
    count
}

从 0.4.1 版本开始，Solver 有 iter()。因此，您可以迭代满足的 'solution: Vec<i32>'，如下所示

#[cfg(feature = "incremental_solver")]
for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() {
    println!("{}-th answer: {:?}", i, v);
}

    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!();
    }
}

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, two-mode reduction, trail saving, unsafe access

USAGE:
  splr [FLAGS] [OPTIONS] <cnf-file>
FLAGS:
  -h, --help                Prints help information
  -C, --no-color            Disable coloring
  -q, --quiet               Disable any progress message
  -c, --certify             Writes a DRAT UNSAT certification file
  -j, --journal             Shows log about restart stages
  -l, --log                 Uses Glucose-like progress report
  -V, --version             Prints version information
OPTIONS:
      --cl <c-cls-lim>      Soft limit of #clauses (6MC/GB)         0
      --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