Lib.rs

ipasir-sys

一个包含 IPASIR 兼容 SAT 求解器 FFI 绑定的 Rust 包。

此包公开了 Rust 到 C 的最小低级接口 ipasir.h。不多也不少。它不尝试提供安全的包装或高级抽象。这些可以在本包之上构建，遵循 *-sys 命名约定，如 这篇文章 中所述。或者，您可以使用 ipasir-rs 包，该包确实提供了这些功能。

如果未指定求解器，此包将尝试构建 Cadical，并具有集成测试来验证绑定是否工作。

什么是 IPASIR？

IPASIR 是增量 SAT 求解器的标准接口。它是 Re-entrant Incremental Satisfiability Application Program Interface 的逆缩写，并在 2015 年年度 SAT 比赛 中引入。

更多解释可以在 这篇论文 的第 6.2 节中找到。

如何使用此包

有两种方式可以使用此包

1. 您可以提供自己的实现 IPASIR 的求解器的静态库
2. 您什么都不做，包将尝试构建和链接 Cadical

最终结果是一样的。IPASIR 函数可以通过在它们周围包装 unsafe 块来调用

use ipasir_sys::*;

fn main() {
    unsafe {
      let solver = ipasir_init();

      ipasir_add(solver, 1);
      ipasir_add(solver, 0);

      let sat_status = ipasir_solve(solver);
      assert_eq!(sat_status, 10);
    }
}

有关更全面的示例，请参阅 coloring_test.rs 或参考 interface_test.rs。

提供自己的库

您可以在构建时设置 IPASIR 环境变量来提供自己的静态库

$ IPASIR=/path/to/libsolver.a cargo build

包将把库复制到其构建目录并尝试链接它。您必须使用绝对路径，但库的名称无关紧要。如果您的库有其他依赖项，建议您将其内联到静态库中。或者，您可以通过 cargo 尝试传递额外的链接标志。

使用 Cadical

如果未设置 IPASIR 环境变量，构建将尝试编译 Cadical 的一个版本，该版本作为构建的一部分。如果不起作用，请尝试从 GitHub 克隆此构建，并单独运行 cargo test。查看 Travis CI 构建和 其配置 可能也有帮助。

如果无法解决问题，请 创建一个问题。

改进建议

• 提供更多求解器并轻松切换它们
• 改进操作系统支持（例如 Windows）
• 添加针对不同求解器和平台的自动化测试

许可证

此构建拥有 MIT 许可证，但在使用之前，请检查所提供软件的许可证限制。