- 主题:用 SMT 会上瘾
自从半年前第一次用 z3 之后，现在做任何优化或者调度的任务，首先想能不能用 z3 解决。Constraints based programming 很符合偷懒的思维方式。
#发自zSMTH@Moto Z3 Play
--
FROM 188.67.236.*
不过这种方法也就是适合优化或者更广泛的说， lattice 中 fixed point 存在性的一类问题。而实际上还是用构造性的方法来解决更有安全感和成就感。
【 在 philbloo 的大作中提到: 】
:
: 自从半年前第一次用 z3 之后，现在做任何优化或者调度的任务，首先想能不能用 z3 解决。Constraints based programming 很符合偷懒的思维方式。
: #发自zSMTH@Moto Z3 Play
#发自zSMTH@Moto Z3 Play
--
FROM 188.67.236.*
不错
--
FROM 119.248.182.*
求科普
--
FROM 101.93.78.*
很简单的概念 就是凡是可以用 linear programming 解决的问题 都可以用 smt 解决 手写的部分只需要列出 constraints 也就是对每个变量列出取值范围和相互关系 然后存在性和最优化的问题都不用手写算法了
【 在 Madlee 的大作中提到: 】
:
: 求科普
#发自zSMTH@Moto Z3 Play
--
FROM 188.67.236.*