Once I understand this, this will be a tutorial on building a simple SATor SMT solver - with inspiration from Pete's class. I can revisit thearticle then.

The Assembly Language ofSatisfiability:Are we bad at SAT solvers? Where are we? How do we bring their power topeople? (To me, this problem is a subset of the "make programmingaccessible" problem, so it's not noteworthy.)

SAT solvers

Cons

• Require input problem to be a propositional logic formula inconjunctive normal form (CNF). This is not a natural way to expressmost problems that require SAT
• Computing CNF formulas is often bad and hard so SAT solvers aren'treally at the right "level" for use by the working programmer
• Look up \`cardinality constraints CNF\` on google scholar - revealslots 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 otherdatatypes, as well as common operations on those types, withoutrequiring a specific normal form!
• API that allows for the manipulation of the input formula exposed bythe solver, unlike strict

How do they work?

Bit blasting

• Directly convert input formula into an equivalent Boolean formula inCNF
• Limited to formulas where every data type has a finite set of values
• Need a SAT solver as a backend, any improvement to SAT translatesdirectly to an improvement to an SMT solver - so this is justadditional tooling around a SAT solver to make it much easier to use.

CDCL(T)

• Definition: conflict driven cause learning - the algorithm employed bymost modern SAT solvers.