Debug-SAT

A debuggable automatic theorem prover for boolean satisfiability problems (SAT).

Brought to you by the AdvancedResearch Community.

Designed for debugging and introspection rather than performance.

NB! This library might contain bugs. Do not use in safety critical applications!

This library can be used to:

• Learn basic logic theorem proving
• Design and verify boolean circuits
• Create machine checked proofs in propositional calculus for many variables
• Used as theorem prover assistant by using tactics step by step
• Optimize partial proofs by selecting from equivalent expressions

How to use it

The Graph::var method adds a new variable. Give it a unique id.

When creating a gate, you use the variables of previously created gates.

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);

There is one method for the following 5 logical gates (selected for readability):

• AND
• OR
• NOT
• EQ
• IMPLY

Other gates are considered less readable, but can be created by combining these 5 gates. For example, if you need XOR, use not(eq(a, b)).

By default, variables and expressions have no value, which are added by making assumptions. An assumption is added to a history stack and can be undoed or inverted.

There are two kinds of assumptions: Equality and inequality. Instead of saying that a variable a is true, you say that a is equivalent to true or not equivalent to false.

The Graph::are_eq method is used to check the value of an variable or expression.

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)`

When you add new stuff to the theorem prover, it does not automatically know the right answer. This requires executing tactics or solving (runs all tactics).

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));

For more information about tactics do, see the Proof enum.