msoos/cryptominisat

[](https://opensource.org/licenses/MIT)  # CryptoMiniSat SAT 求解器 该系统提供 CryptoMiniSat，这是一个先进的增量 SAT 求解器。 该系统具有 3 个接口：命令行、C++ 库和 Python。命令行 接口接受一个 [cnf](http://en.wikipedia.org/wiki/Conjunctive_normal_form) 作为输入，格式为 [DIMACS](http://www.satcompetition.org/2009/format-benchmarks2009.html) 并支持 XOR 子句的扩展。C++ 和 Python 接口模仿此行为， 也允许增量使用：假设和多次 `solve` 调用。还提供了一个兼容 C 和 Rust 的包装器。 在引用时，请始终参考我们的 [SAT 2009 会议论文](https://link.springer.com/chapter/10.1007%2F978-3-642-02777-2_24)， 参考文献记录位于 [这里](http://dblp.uni-trier.de/rec/bibtex/conf/sat/SoosNC09)。 ## 编译 建议使用 [release 二进制文件](https://github.com/msoos/cryptominisat/releases)。次选方案是使用 Nix。只需 [安装 nix](https://nixos.org/download/)，然后执行： ``` nix shell github:msoos/cryptominisat ``` 然后你将拥有 `cryptominisat` 二进制文件并可直接使用。 你也可以在无需安装任何内容的情况下，通过浏览器运行 CryptoMiniSat，[点击这里](https://www.msoos.org/cryptominisat/)。 ### 从源代码构建 首先安装系统依赖： ``` # Debian/Ubuntu sudo apt-get install build-essential cmake git libgmp-dev # macOS (brew) brew install cmake gmp ``` 然后进行构建 — cadical 和 cadiback 会自动获取并编译： ``` git clone https://github.com/msoos/cryptominisat cd cryptominisat mkdir build && cd build cmake .. make -j8 ``` 如果你已经构建了 cadical 和 cadiback，可以指向 cmake 以跳过自动获取： ``` cmake .. -Dcadical_DIR=/path/to/cadical/build -Dcadiback_DIR=/path/to/cadiback make -j8 ``` ### 在 Windows 上构建（MSYS2/MINGW64） 安装 [MSYS2](https://www.msys2.org/)，然后在 MINGW64 shell 中安装依赖： ``` pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-cmake mingw-w64-x86_64-ninja \ mingw-w64-x86_64-make mingw-w64-x86_64-gmp mingw-w64-x86_64-zlib make ``` 然后构建： ``` git clone --recurse-submodules https://github.com/msoos/cryptominisat cd cryptominisat mkdir build && cd build cmake -G Ninja -DCMAKE_BUILD_TYPE=Release .. cmake --build . -v ``` 若要生成完全静态的二进制文件（运行时无外部 DLL 依赖），添加 `-DBUILD_SHARED_LIBS=OFF`： ``` cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=OFF .. cmake --build . -v ``` ## 命令行用法 以以下文件为例： ``` p cnf 3 3 1 0 -2 0 -1 2 3 0 ``` 该文件包含 3 个变量和 3 个子句，这在头部 `p cnf 3 3` 中体现，分别表示变量数量和子句数量。每个子句以 '0' 结尾。子句含义为：1 必须为真，2 必须为假，且 1 必须为假、2 必须为真 或 3 必须为真。该问题的唯一解为： ``` cryptominisat5 --verb 0 file.cnf s SATISFIABLE v 1 -2 3 0 ``` 这意味着将变量 1 设为真、变量 2 设为假、变量 3 设为真，可满足 CNF 中的约束条件。若文件内容为： ``` p cnf 3 4 1 0 -2 0 -3 0 -1 2 3 0 ``` 则问题无解，求解器将返回 `s UNSATISFIABLE`。 ## 增量 Python 用法 该 Python 模块兼容 Python 3。只需执行： ``` pip3 install pycryptosat ``` 随后可按如下方式以增量模式使用： ``` >>> from pycryptosat import Solver >>> s = Solver() >>> s.add_clause([1]) >>> s.add_clause([-2]) >>> s.add_clause([-1, 2, 3]) >>> sat, solution = s.solve() >>> print(sat) True >>> print(solution) (None, True, False, True) >>> sat, solution = s.solve([-3]) # assume var 3 = False → UNSAT >>> print(sat) False >>> sat, solution = s.solve() # without assumption → still SAT >>> print(sat) True >>> s.add_clause([-3]) # permanently add -3 >>> sat, solution = s.solve() >>> print(sat) False ``` 若要从源代码构建 Python 包，构建过程会使用 [scikit-build-core](https://github.com/scikit-build/scikit-build-core)， 它会自动驱动 CMake 并获取、编译 cadical 和 cadiback，因此无需手动安装 C++ 依赖（GMP 除外）。 ``` # Debian/Ubuntu sudo apt-get install build-essential cmake libgmp-dev python3-dev # macOS brew install cmake gmp git clone https://github.com/msoos/cryptominisat cd cryptominisat python3 -m venv venv source venv/bin/activate pip install scikit-build-core cmake ninja build pip install . --no-build-isolation ``` 或者在不安装的情况下生成 wheel 文件： ``` python -m build --wheel --no-isolation # wheel lands in dist/ pip install dist/pycryptosat-*.whl ``` ### 增量库用法 库使用的变量编号从 0 开始。由于 0 不能被取反，因此使用类 `Lit` 表示：`Lit(variable_number, is_negated)`。因此，上述第一个 CNF 可表示为： ``` #include #include #include using std::vector; using namespace CMSat; int main() { SATSolver solver; vector clause; //Let's use 4 threads solver.set_num_threads(4); //We need 3 variables. They will be: 0,1,2 //Variable numbers are always trivially increasing solver.new_vars(3); //add "1 0" clause.push_back(Lit(0, false)); solver.add_clause(clause); //add "-2 0" clause.clear(); clause.push_back(Lit(1, true)); solver.add_clause(clause); //add "-1 2 3 0" clause.clear(); clause.push_back(Lit(0, true)); clause.push_back(Lit(1, false)); clause.push_back(Lit(2, false)); solver.add_clause(clause); lbool ret = solver.solve(); assert(ret == l_True); std::cout << "Solution is: " << solver.get_model()[0] << ", " << solver.get_model()[1] << ", " << solver.get_model()[2] << std::endl; //assumes 3 = FALSE, no solutions left vector assumptions; assumptions.push_back(Lit(2, true)); ret = solver.solve(&assumptions); assert(ret == l_False); //without assumptions we still have a solution ret = solver.solve(); assert(ret == l_True); //add "-3 0" //No solutions left, UNSATISFIABLE returned clause.clear(); clause.push_back(Lit(2, true)); solver.add_clause(clause); ret = solver.solve(); assert(ret == l_False); return 0; } ``` 库调用也支持假设。我们可以在上述代码的 `return 0;` 前添加以下行： ``` vector assumptions; assumptions.push_back(Lit(2, true)); lbool ret = solver.solve(&assumptions); assert(ret == l_False); ret = solver.solve(); // no assumption → solution exists again assert(ret == l_True); ``` 由于我们假设变量 2 必须为假，因此无解。但若再次求解（不带假设），则会恢复原始解。 假设允许我们在**单次运行**中假设某些文字的值，但并非所有运行——对于所有运行，可以简单地将这些假设作为长度为 1 的子句添加。 ## 多解求解 要查找问题的多个解，只需循环运行求解器并排除已找到的解： ``` while(true) { lbool ret = solver->solve(); if (ret != l_True) { assert(ret == l_False); //All solutions found. exit(0); } //Use solution here. print it, for example. //Banning found solution vector ban_solution; for (uint32_t var = 0; var < solver->nVars(); var++) { if (solver->get_model()[var] != l_Undef) { ban_solution.push_back( Lit(var, (solver->get_model()[var] == l_True)? true : false)); } } solver->add_clause(ban_solution); } ``` 上述循环将持续运行，直到没有更多解为止。**强烈建议**仅将**重要或主要变量**添加到新子句（`ban_solution`）中。不应添加仅用于将原始问题转换为 CNF 的变量。这样可避免产生与主要变量无关的虚假解。 ## Rust 绑定 要构建 Rust 绑定： ``` git clone https://github.com/msoos/cryptominisat-rs/ cd cryptominisat-rs cargo build --release cargo test ``` 你可以按照该 [README](https://github.com/msoos/cryptominisat-rs/blob/master/README.markdown) 使用。在 Rust 项目中引入 CryptoMiniSat，需在 `Cargo.toml` 中添加依赖： ``` cryptominisat = { git = "https://github.com/msoos/cryptominisat-rs", branch= "master" } ``` 你可以在 [此处](https://github.com/msoos/caqe/) 查看使用 CryptoMiniSat 的 Rust 示例项目。 ## 预处理 若希望将 CryptoMiniSat 用作预处理器，建议尝试我们的模型计数预处理器 [Arjun](https://www.github.com/meelgroup/arjun)。 ## 高斯消元 从 CryptoMiniSat 5.8 开始，高斯消元默认编译进求解器。但若求解器检测到高斯消元表现不佳，会自动关闭。要使用高斯消元，请提供包含 XOR 的 CNF（可以是纯 CNF 或 XOR+CNF 格式），并使用默认设置运行， 或按需调整： ``` Gauss options: --iterreduce arg (=1) Reduce iteratively the matrix that is updated.We effectively are moving the start to the last column updated --maxmatrixrows arg (=3000) Set maximum no. of rows for gaussian matrix. Too large matrixes should be discarded for reasons of efficiency --autodisablegauss arg (=1) Automatically disable gauss when performing badly --minmatrixrows arg (=5) Set minimum no. of rows for gaussian matrix. Normally, too small matrixes are discarded for reasons of efficiency --savematrix arg (=2) Save matrix every Nth decision level --maxnummatrixes arg (=3) Maximum number of matrixes to treat. ``` 特别是，如果确定有帮助，可以设置 `--autodisablegauss 0`。 ## 证明验证 CryptoMiniSat 可以输出 FRAT 证明，可独立验证。运行求解器并指定证明输出文件： ``` ./cryptominisat5 input.cnf proof.frat ``` 然后使用 [meelgroup/frat-xor](https://github.com/meelgroup/frat-xor) 中的工具进行细化与检查： ``` grep -v "^c" proof.frat > proof_clean.frat ./frat-xor elab proof_clean.frat input.cnf proof.xlrup ./cake_xlrup input.cnf proof.xlrup ``` `cake_xlrup` 成功后输出 `s VERIFIED`。更多细节（包括调试验证失败）请参考 [README_VERIFIER.md](README_VERIFIER.md)。 ## CMake 参数 以下参数用于配置生成的构建产物。在运行 `make` 前指定选项：`cmake ..` - `-DBUILD_SHARED_LIBS=` — 构建共享（ON，默认）或静态（OFF）库与二进制文件。 - `-DSTATS=` — 高级统计信息（会降低性能）。需要安装 [louvain communities](https://github.com/meelgroup/louvain-community)。 - `-DENABLE_TESTING=` — 启用测试套件。 - `-DLARGEMEM=` — 为子句分配更多内存（但对多数问题会变慢）。 - `-DIPASIR=` — 构建 `libipasircryptominisat.so` 以支持 [IPASIR](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/IPASIR____IPASIR) 接口。 - `-Dcadical_DIR=` — 指向已构建的 CaDiCaL `build/` 目录（包含 `libcadical.a`）。若未设置，将自动获取并构建。 - `-Dcadiback_DIR=` — 指向已构建的 CaDiBaCk 目录（包含 `libcadiback.a`）。若未设置，将自动获取并构建。 ## C 语言用法 详见 src/cryptominisat_c.h.in。此为实验性功能。 ## 许可证 默认构建所需的一切均采用 MIT 许可证。如果你 明确指示系统使用 Bliss（两者均为 GPL 许可证）， 但默认情况下 CryptoMiniSat 不会启用这些组件。

标签：Bash脚本, C++库, C绑定, DIMACS, Nix, Rust绑定, SAT求解器, Web界面, XOR子句, 优化, 可满足性, 可视化界面, 增量求解, 密码学, 开源, 开源框架, 手动系统调用, 持续集成, 搜索引擎优化, 构建系统, 约束求解, 逆向工具