CryptoMiniSat的Rust绑定

这为CryptoMiniSat提供了一个Rust绑定，它是一个开源的SAT求解器，用C++编写。您可以在这里找到更多关于它的信息。要构建

git clone https://github.com/msoos/cryptominisat-rs
cd cryptominisat-rs
git submodule init
git submodule update --init
cargo build --release
cargo test

基本用法

以下是基本用法的示例。

extern crate cryptominisat;
use cryptominisat::*;

fn main() {
    let mut s = Solver::new();
    s.set_num_threads(4);

    let x = s.new_var();
    let y = s.new_var();
    let z = s.new_var();

    s.add_clause(&[x]);
    s.add_clause(&[!y]);
    s.add_clause(&[!x, y, z]);

    assert!(s.solve() == Lbool::True);
    assert!(s.is_true(x));
    assert!(s.is_true(!y));
    assert!(s.is_true(z));
}

变量通过无符号整数0...n-1进行索引。一个文字代表变量或否定变量。一个子句是一组文字，其中至少有一个必须在最终解中为真。为了方便，new_var()既添加变量又返回表示新变量的文字。但是，如果您愿意，可以手动创建文字和子句。上面的代码是以下代码的语法糖。

    let mut solver = Solver::new();
    let mut clause = Vec::new();

    solver.set_num_threads(4);
    solver.new_vars(3);

    clause.push(Lit::new(0, false).unwrap());
    solver.add_clause(&clause);

    clause.clear();
    clause.push(Lit::new(1, true).unwrap());
    solver.add_clause(&clause);

    clause.clear();
    clause.push(Lit::new(0, true).unwrap());
    clause.push(Lit::new(1, false).unwrap());
    clause.push(Lit::new(2, false).unwrap());
    solver.add_clause(&clause);

    let ret = solver.solve();
    assert!(ret == Lbool::True);
    assert!(solver.get_model()[0] == Lbool::True);
    assert!(solver.get_model()[1] == Lbool::False);
    assert!(solver.get_model()[2] == Lbool::True);

注意，当n >= 2^31时，Lit::new()返回None，但Cryptominisat本身对MAX_NUM_VARS的极限要低得多，目前为2^28 - 1。

假设

库的使用还允许假设。一个假设告诉求解器，给定的文字应该假设为真，仅此一次运行。这与通过add_clause()添加不同，因为它可以很容易地撤销，并从求解器以前的工作中受益，而移除已添加的子句则需要重新创建整个求解器，并丢弃所有内部保存的进度。在以下示例中，假设不同的值会导致b和d的值也发生变化。

    let mut s = Solver::new();
    let a = s.new_var();
    let b = s.new_var();
    let c = s.new_var();
    let d = s.new_var();

    s.add_clause(&[a, b, !c]);
    s.add_clause(&[a, !b, c]);
    s.add_clause(&[!a, b, c]);
    s.add_clause(&[!a, !b, !c]);

    s.add_clause(&[!d, b, !c]);
    s.add_clause(&[!d, !b, c]);
    s.add_clause(&[d, b, c]);
    s.add_clause(&[d, !b, !c]);

    s.add_clause(&[a, d, !c]);
    s.add_clause(&[a, !d, c]);
    s.add_clause(&[!a, d, c]);
    s.add_clause(&[!a, !d, !c]);

    assert!(s.solve_with_assumptions(&[a]) == Lbool::True);
    assert!(s.is_true(a));
    assert!(s.is_true(!b));
    assert!(s.is_true(c));
    assert!(s.is_true(!d));

    assert!(s.solve_with_assumptions(&[!a]) == Lbool::True);
    assert!(s.is_true(!a));
    assert!(s.is_true(b));
    assert!(s.is_true(c));
    assert!(s.is_true(d));

异或子句

除了传统的OR子句之外，Cryptominisat还支持XOR子句。这些子句需要额外的bool参数rhs，它给出所有指定文字异或的结果的预期值。例如，以下行强制执行约束，即a为真或d为假，但不能同时为真。如果第二个参数是false而不是true，则它要求要么a为真且d为假，要么a为假且d为真。

    s.add_xor_literal_clause(&[a, !d], true);

错误处理

Cryptominisat通过将消息写入stderr然后终止来处理错误。如果您想使用恐慌，应该编写一个包装器，它可以在之前检测到不正确的使用并引发恐慌。可能引起错误的条件的不完整列表包括

• 将0传递给set_num_threads()
• 在调用任何其他方法之后调用set_num_threads()
• 创建太多变量
• 传递一个尚未添加到求解器的变量

许可

MIT