sat

Rust中定义和解决布尔可满足性（SAT）问题的接口。

文档

lib.rs:

定义和解决SAT问题的接口。

布尔可满足性问题（简称SAT）询问，对于给定的布尔公式，是否存在对公式变量的赋值（真或假），使得公式评估为真。

SAT是NP完全，这意味着两件事

1. 许多重要问题（例如在程序分析、电路设计或物流规划中）可能被视为SAT的实例。

2. 人们相信不存在一种算法可以有效地解决所有SAT的实例。

尽管（2）存在，但观察（1）是重要的，因为存在一些算法（如DPLL）可以有效地解决实践中遇到的SAT实例。

这个crate允许用户制定SAT的实例，并使用现成的SAT求解器来解决它们。

// Create a SAT instance.
let mut i = sat::Instance::new();
let x = i.fresh_var();
let y = i.fresh_var();
let z = i.fresh_var();
i.assert_any(&[x, z]);        //     (x OR z)
i.assert_any(&[!x, !y, !z]);  // AND (!x OR !y OR !z)
i.assert_any(&[y]);           // AND (y = TRUE)

// Use the external program `minisat` as a solver.
let s = sat::solver::Dimacs::new(|| Command::new("minisat"));

// Solve the instance and check that it meets our requirements.
let a = s.solve(&i).unwrap();
assert!(a.get(x) || a.get(z));
assert!(!a.get(x) || !a.get(y) || !a.get(z));
assert!(a.get(y));

// Add a clause which makes the instance impossible to satisfy,
// and check that the solver recognizes as much.
i.assert_any(&[!y]);
assert!(s.solve(&i).is_none());

要查看更详细的示例，请参阅examples/petersen.rs，该文件生成Petersen图的3色图。