SMT
Once I understand this, this will be a tutorial on building a simple SAT
or SMT solver - with inspiration from Pete's class. I can revisit the
article then.
[The Assembly
Language of Satisfiability]: Are we bad at SAT solvers? Where are we?
How do we bring their power to people? (To me, this problem is a subset of the
"make programming accessible" problem, so it's not noteworthy.)
SAT solvers
Cons
- Require input problem to be a propositional logic formula in
conjunctive normal form (CNF). This is not a natural way to express most
problems that require SAT
- Computing CNF formulas is often bad and hard so SAT solvers aren't
really at the right "level" for use by the working programmer
- Look up
on google scholar - reveals lots of problems and tradeoffs that
can be made
Why SMT over SAT?
- SMT solvers allow more freedom in the expression of input problems -
support integers, fixed width floats, arrays and potentially other datatypes, as
well as common operations on those types, without requiring a specific normal
form!
- API that allows for the manipulation of the input formula exposed by
the solver, unlike strict
How do they work?
Bit blasting
- Directly convert input formula into an equivalent Boolean formula in
CNF
- Limited to formulas where every data type has a finite set of values
- Need a SAT solver as a backend, any improvement to SAT translates
directly to an improvement to an SMT solver - so this is just additional tooling
around a SAT solver to make it much easier to use.
CDCL(T)
- Definition: conflict driven cause learning - the algorithm employed by
most modern SAT solvers.