Proofs SAT Boolean Circuits SMT
Posted on May 1, 2014
Tags: othermath
1 Proof vs SAT
How does boolean satisfiability relate to proofs?
- In proofs we build a tree growing downwards.
- The top are leaves that can vary in truth and false like \(P \rightarrow Q\) and \(P\).
- HOWEVER, the root aka the result of the proof tree \((P \rightarrow Q) \rightarrow P \rightarrow Q\) will ALWAYS BE A TAUTOLOGY NO MATTER HOW MUCH WE VARY THE LEAVES
- The top are leaves that can vary in truth and false like \(P \rightarrow Q\) and \(P\).
| \(P \rightarrow Q\) | \(P\) | \((P \rightarrow Q) \rightarrow P \rightarrow Q\) |
|---|---|---|
| 1 | 1 | 1 |
| 1 | 0 | 1 |
| 0 | 1 | 1 |
| 0 | 0 | 1 |
If we can build a proof of a statement, we know the expression is Satisfiable. Not only satisfiable but tautologically true (as shown in the third column representing the output)
- A SAT SOLVER tries all possible input models, checks if one of the those models results in a true output. Aka it’s literally just building a truth table and scanning the output column.
- Notice the expression only needs 1 true output to be satisfiable; it does not need to be true for ALL outputs aka tautology
- Trivially extend 3SAT so it can tell you if a output statement is tautologically true, AKA true for all input models.
- In this case, such a expression is a candidate for having a proof.
2 Circuits
What happens if we built a circuit like a proof?
It would be useless since any input we give this circuit will be true like a lightbulb that stays on no matter what switch you pull. (Remember a proof is a tautology, true for all input states)
3 SMT
SMT is closely related to SAT.
Imagine instead of just Boolean variables, we had strings, arrays, real numbers, quantifiers in the expression of interest.
SMT solver is the first-order logic equivalent of SAT solver
