### 4 releases (breaking)

Uses old Rust 2015

0.4.0 | Feb 14, 2018 |
---|---|

0.3.0 | Feb 10, 2018 |

0.2.0 | Feb 10, 2018 |

0.1.0 | Feb 10, 2018 |

#**769** in Math

**MIT**license

69KB

1.5K
SLoC

# 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

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

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

is `a`

,
you say that `true`

is equivalent to `a`

or not equivalent to `true`

.`false`

The

method is used to check the value of an variable or expression.`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)`

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

enum.`Proof`