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](https://jix.one/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 \`cardinality constraints CNF\` 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.