SAT in real programming scenario

Question

I read about SAT and SMT. I always wonder how it can be applied in real programming scenario.

Here is an example:

Given that var a = 20; var b = a; are true, we want to know if b = 20 is true or false.

How should I turn it into boolean algebra expressions and apply SAT?

Answer 1

Here is the simplest example using SMT-LIB 2.0 standard supported by many SMT solvers:

(declare-fun a () Int)
(declare-fun b () Int)
(assert (= a b))
(assert (= a 20))
(assert (= b 20))
(check-sat)

You can use http://rise4fun.com/z3 to experiment with it. It will respond "sat" meaning the assertions can be satisfied, meaning then b can be 20.

Then you can replace (assert (= b 20)) with (assert (distinct b 20)). Z3 will respond with "unsat" meaning it's not possible for b to be anything else.