对于如何根据最终得到的结果求解输入向量，已经有很多现成的数学工具可以使用，这些工具底层原理是

• SAT（Boolean satisfiability problem)）
• SMT（Satisfiability Modulo Theory）可满足性模理论

SMT-solvers are frontends to SAT solvers, i.e., they translate inputted SMT expressions into CNF and feed SAT-solver with it.

One can say that a SMT solver is a library of various methods on top of a SAT solver.

SMT vs. SAT is like high level PL vs. assembly language.

SMT-Solvers

• Yices
• Z3
• CVC3/CVC4
• STP
• Boolector
• ……

Manticore 默认使用的Yices

Mythril 默认使用的Z3

SMTChecker是Solidity编译器中的形式验证模块，默认也用的Z3