rsat-cli

SolHop SAT Solver.

目前，已经实现了基于probSAT的随机局部搜索和基于MiniSAT的CDCL求解器。更多算法将很快可用。

该项目仍在开发中。在第一个稳定版本v1.0.0发布之前，API可能会发生很大变化。

安装和运行

安装

cargo install rsat-cli

帮助

$ rsat --help
rsat 0.1.0
SolHOP SAT Solver

USAGE:
    rsat [FLAGS] [OPTIONS] <file>

FLAGS:
    -h, --help        Prints help information
    -p, --parallel    Enables data parallelism (currently only for sls solver)
    -V, --version     Prints version information

OPTIONS:
    -a, --alg <alg>                Algorithm to use (1 -> CDCL, 2 -> SLS) [default: 1]
        --max-flips <max-flips>    Maxinum number of flips in each try of SLS [default: 1000]
        --max-tries <max-tries>    Maximum number of tries for SLS [default: 100]

ARGS:
    <file>    Input file in DIMACS format

用法

rsat input.cnf -a 1

其中 input.cnf 是以DIMACS格式输入的SAT实例。使用 -a 2 来调用SLS求解器。有关一些选项，请参阅帮助。

以下是一些示例

示例 1

输入

c comment
p cnf 3 4
1 0
-1 -2 0
2 -3 0
-3 0

输出

SAT
1 -2 -3 0

示例 2

输入

c comment
p cnf 3 4
1 0
-1 -2 0
2 -3 0
3 0

输出

UNSAT

注意：SLS求解器永远不会被用于证明UNSAT。它将给出迄今为止找到的最佳模型。

UNKNOWN
-1 2 3 0

许可证

MIT