Debug-SAT

布尔可满足性问题（SAT）的调试自动定理证明器。

由 AdvancedResearch 社区 提供。

设计用于调试和内省，而非性能。

注意！此库可能包含错误。不要用于关键安全应用！

此库可用于

• 学习基本的逻辑定理证明
• 设计和验证布尔电路
• 在命题演算中为多个变量创建机器验证证明
• 通过逐步使用策略作为定理证明器助手
• 通过选择等价表达式来优化部分证明

如何使用它

Graph::var 方法添加一个新变量。给它一个唯一的ID。

创建门时，您使用之前创建的门变量。

use debug_sat::Graph;

let ref mut graph = Graph::new();
let a = graph.var(0);
let b = graph.var(1);
let a_and_b = graph.and(a, b);

以下5个逻辑门有一个方法（为可读性选择）

• AND
• OR
• NOT
• EQ
• IMPLY

其他门被认为可读性较差，但可以通过组合这5个门来创建。例如，如果需要XOR，请使用 not(eq(a, b))。

默认情况下，变量和表达式没有值，这些值通过假设添加。假设添加到历史堆栈中，可以撤销或反转。

有两种假设：等式和不等式。您不说变量 a 是 true，而是说 a 等价于 true 或不等价于 false。

使用 Graph::are_eq 方法检查变量或表达式的值。

use debug_sat::Graph;

let ref mut graph = Graph::new();
let a = graph.var(0);
let tr = graph.true_();
let a_is_tr = graph.assume_eq(a, tr);
assert_eq!(graph.are_eq(a, tr), Some(true));
a_is_tr.undo(graph); // Alternative: `a_is_tr.invert(graph)`

当您向定理证明器添加新内容时，它不会自动知道正确答案。这需要执行策略或解决（运行所有策略）。

use debug_sat::{Graph, Proof};

let ref mut graph = Graph::new();
let a = graph.var(0);
let b = graph.var(1);
let a_and_b = graph.and(a, b);
let a_is_b = graph.assume_eq(a, b);
// Does not know that `and(a, b) = a` when `a = b`.
assert_eq!(graph.are_eq(a_and_b, a), None);
// Run the tactic that checks input to AND is EQ.
// This is how the theorem prover learns, by checking stuff.
// Alternative: `graph.solve()` runs all tactics until nothing new is learned.
assert_eq!(graph.eq_and(a_and_b), Proof::True);
// Now the theorem prover knows the answer.
assert_eq!(graph.are_eq(a_and_b, a), Some(true));

有关策略的更多信息，请参阅 Proof 枚举。