Zenn
Open5

SATソルバー"splr"を使おう

Rust
#
sat
#
satsolver
hysok2hysok2

splrを使ってみます。過程で現れた覚書をスクラップにしたためます。

hysok2hysok2

splrとは

SATソルバーのひとつです。Rustで書かれています。結構アクティブに開発されているみたいで、最後の更新は2022年9月です。

SATソルバーとは

SAT問題を自動で解くソフトウェアです。ここで、SAT問題とは、Conjunctive normal formで書かれた論理式を充足する変数の値があるかを判定し、値がある場合はそれらを見つける問題です。

Rustで書かれたSATソルバーでは、varisatが人気です。こちらは最後のリリースが2019年5月です。

なぜsplrを試そうとしたか

アクティブに更新されているようなので、今まで使っていたvarisatより性能が良いのではないかと思ったからです。

hysok2hysok2

不思議な挙動

自明な充足不可能な論理式を渡しソルバーに解かせると、充足不可能を表す

Certificate::UNSAT

ではなく、

SolverError::EmptyClause

が返ってくるときがあります。
例えば、"X && !X"という論理式を判定すべく、以下のコードを動かすと、

use splr::*;

fn main() {
    let v: Vec<Vec<i32>> = vec![vec![1], vec![-1]];
    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),
    }
}

以下のメッセージのとおりエラーとなってしまいます。

thread 'main' panicked at 's UNKNOWN; EmptyClause', src/main.rs:8:19
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

個人的には、UNSATが返って欲しいですが、エラーが返ってきてしまう。しかもエラーの説明が「空の項」です。多分、前処理かなにかで自明なリテラルは消されちゃって、ソルバーそのものにはリテラルのない空の項が渡ってしまっているのだと思います。

もう少しコードを深掘りして見てみます。

hysok2hysok2

splrとvarisatを比較

実験環境

windows 10 - wsl2 - ubuntu 20.04
CPU: Ryzen5 3500U, メモリ:20GB

実行時間

$ time splr sample.cnf
sample.cnf                                         250,1065 |time:     0.25
 #conflict:      14576, #decision:       122835, #propagate:         950341
  Assignment|#rem:      243, #fix:        1, #elm:        6, prg%:   2.8000
      Clause|Remv:     1181, LBD2:       46, BinC:        0, Perm:     1055
    Conflict|entg:   6.7219, cLvl:  11.9680, bLvl:  10.8542, /cpr:     8.47
    Learning|avrg:   7.8125, trnd:   0.9988, #RST:     8295, /dpc:     1.45
        misc|vivC:       15, subC:        0, core:      106, /ppc:    47.33
      Result|file: ./ans_sample.cnf
s SATISFIABLE: sample.cnf

real    0m0.268s
user    0m0.257s
sys     0m0.000s
$ time varisat sample.cnf
c This is varisat 0.2.1
c   release build - rustc 1.65.0 (897e37553 2022-11-02)
c Reading file 'sample.cnf'
c Parsed formula with 250 variables and 1065 clauses
c confl: 5k rest: 21 vars: 250 bin: 0 irred: 1065 core: 249 mid: 1080 local: 3671
c confl: 10k rest: 31 vars: 250 bin: 0 irred: 1065 core: 446 mid: 2240 local: 7314
c confl: 15k rest: 51 vars: 250 bin: 0 irred: 1065 core: 688 mid: 3454 local: 10858
c confl: 20k rest: 62 vars: 250 bin: 0 irred: 1065 core: 911 mid: 5050 local: 8610
c confl: 25k rest: 66 vars: 250 bin: 0 irred: 1065 core: 1127 mid: 5183 local: 13261
c confl: 30k rest: 85 vars: 250 bin: 0 irred: 1065 core: 1384 mid: 6465 local: 16722
c confl: 35k rest: 96 vars: 250 bin: 0 irred: 1065 core: 1609 mid: 5740 local: 13861
c confl: 40k rest: 116 vars: 250 bin: 2 irred: 1065 core: 1864 mid: 7750 local: 16594
c confl: 45k rest: 125 vars: 250 bin: 2 irred: 1065 core: 2099 mid: 6425 local: 22684
c confl: 50k rest: 127 vars: 250 bin: 3 irred: 1065 core: 2353 mid: 8613 local: 13899
c confl: 55k rest: 127 vars: 250 bin: 5 irred: 1065 core: 2550 mid: 6848 local: 20465
s SATISFIABLE
v 1 -2 3 4 -5 6 7 8 -9 -10 11 12 -13 -14 15 16 -17 18 -19 20 -21 -22 23 -24 25 26 -27 -28 -29 30 -31 -32 -33 34 35 36 -37 38 39 40 41 42 43 44 -45 46 47 48 -49 -50 51 -52 53 -54 55 -56 -57 -58 59 60 -61 62 -63 -64 65 -66 -67 68 69 70 -71 72 -73 -74 75 -76 77 -78 79 80 -81 -82 -83 -84 85 -86 87 88 89 90 91 92 93 -94 -95 96 97 -98 99 -100 101 102 -103 -104 -105 -106 107 108 -109 -110 111 -112 113 114 -115 -116 117 -118 119 -120 -121 122 123 124 125 -126 -127 -128 129 130 131 -132 -133 -134 -135 136 -137 -138 139 -140 141 142 -143 -144 145 -146 -147 -148 149 150 -151 152 -153 154 -155 -156 -157 -158 -159 -160 -161 162 -163 -164 165 166 167 -168 169 170 171 172 173 174 -175 -176 -177 178 179 180 -181 -182 -183 184 -185 186 187 -188 189 -190 191 -192 -193 -194 195 -196 -197 198 199 200 201 -202 203 204 205 206 -207 208 -209 -210 -211 212 -213 -214 215 216 -217 -218 -219 220 -221 -222 223 224 225 -226 -227 -228 -229 -230 -231 -232 -233 234 -235 -236 -237 238 239 240 241 -242 243 244 -245 246 247 -248 -249 -250 0
real    0m2.226s
user    0m2.212s
sys     0m0.000s

$ time splr unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
unif-k3-r4.25-v360-c1530-S1028159446-096.cnf       360,1530 |time:   351.51
 #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
s UNSATISFIABLE: unif-k3-r4.25-v360-c1530-S1028159446-096.cnf

real    5m51.518s
user    5m49.412s
sys     0m2.081s
$ time varisat unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
.....
real    7m9.722s
user    7m9.570s
sys     0m0.141s

splrの勝ちです。