Windosw环境下安装Z3约束求解器并使用Python Binding
Z3 是一个微软出品的开源约束求解器,能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题(可以简单理解为解方程的感觉,虽然这么比喻其实还差距甚远,请勿吐槽),功能强大且易于使用。Z3 约束求解器是针对 Satisfiability modulo theories Problem 的一种
...