SMT(Satisfiability Modulo Theories) logic SAT の値がboolじゃなくなったもの. 有名な solverのひとつは Microsoft z3 Julia bindingもある. SATが命題論理, SMTが一階述語論理に対応しているらしい solverで最適化問題を解く 充足判定を二分探索すること<=>最適化問題を解く