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


  • 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.


  • Definition: conflict driven cause learning - the algorithm employed by most modern SAT solvers.
2022-11-08 ba4b837
2022-11-01 b0115e4
2021-09-22 52a677b
2021-09-21 7732812
2021-08-19 87d9551
2021-05-13 620c52a