LSTECH_MAPLE
介绍
LSTECH_MAPLE 是一款高性能的 SAT 开源求解器，获得了2021年 SAT Competition 中 Main Track SAT 的亚军，能够求解 SAT 和 UNSAT 问题。LSTECH_MAPLE 改进了冲突驱动子句学习（Conflict Driven Clause Learning，CDCL）算法，在松弛了 CDCL 过程的同时加入了 Local Search。LSTECH_MAPLE 由 C++ 开发，支持读写 CNF格式 (opens new window)（Conjunctive Normal Form）的文件。
参数
CORE OPTIONS
| 参数 | 含义 | 默认 |
|---|---|---|
step-size | 初始步长 | 0.40 |
step-size-dec | 步长衰减 | 0.000001 |
min-step-size | 最小步长 | 0.06 |
var-decay | 变量活动衰减因子 | 0.80 |
cla-decay | 子句活动衰减因子 | 0.999 |
rnd-freq | 启发式随机选择变量的频率 | 0 |
rnd-seed | 随机选择变量的随机数种子 | 91648253 |
ccmin-mode | 控制冲突子句的最小化 (0=none, 1=basic, 2=deep) | 2 |
phase-saving | phase saving的等级 (0=none, 1=limited, 2=full) | 2 |
rnd-init | 随机化初始活动 | false |
rfirst | 基础重启的间隔 | 100 |
rinc | 重启间隔增加因子 | 2 |
gc-frac | 触发垃圾内存收集之前允许浪费的内存比例 | 0.20 |
chrono | 控制是否执行时间回溯 | 100 |
confl-to-chrono | 控制执行时间回溯的冲突数量 | 4000 |
DUP-LEARNTS OPTIONS
| 参数 | 含义 | 默认 |
|---|---|---|
lbd-limit | 指定duplicates learnts检测的最大lbd（Literals Blocks Distance）. | 14 |
min-dup-app | 指定加入DB的最小的learnts的数量. | 2 |
dupdb-init | 指定初始的最大duplicates DB的大小. | 1000000 |
MAIN OPTIONS
| 参数 | 含义 | 默认 |
|---|---|---|
verb | 详细的级别（0=silent, 1=some, 2=more） | 1 |
pre | 完全打开/关闭预处理. | true |
dimacs | 如果指定了文件，预处理后就停止并将结果写入该文件. | |
cpu-lim | 最大CPU时间，以秒计. | INT32_MAX = 2147483647 |
mem-lim | 最大内存，以MB计. | INT32_MAX |
drup | 生成DRUP UNSAT证明. | false |
drup-file | DRUP UNSAT证明的输出文件. | "" |
SIMP OPTIONS
| 参数 | 含义 | 默认 |
|---|---|---|
asymm | 通过不对成分支缩小子句. | false |
elim | 执行变量消除. | true |
rcheck | 检查子句是否已被暗含.（运行成本高） | false |
simp-gc-frac | 在简化过程中触发垃圾内存收集之前允许浪费的内存比例. | 0.5 |
grow | 允许一次变量消除所产生的子句数. | 0 |
cl-lim | 如果产生的分解长度超过该值，则不进行变量消除. -1指无限制 | 20 |
sub-lim | 不检查长度大于该值的子句是否与其他子句有包含关系. -1指无限制 | 1000 |
HELP OPTIONS
| 参数 | 含义 |
|---|---|
help | 输出帮助信息. |
help-verb | 输出详细的帮助信息. |
使用示例
./lstech_maple [options] <input-file> <result-output-file>
1
./lstech_maple --help
1
注意：HELP OPTIONS前都要使用--，其余OPTIONS前加-，设定参数时的=前后都不能有空格。
求解CNF文件
./lstech_maple ./input.cnf
1
./lstech_maple -cpu-lim=1000 ./input.cnf ./output.cnf
1
← LEAVES