不过这种方法也就是适合优化或者更广泛的说， lattice 中 fixed point 存在性的一类问题。而实际上还是用构造性的方法来解决更有安全感和成就感。

【 在 philbloo 的大作中提到: 】
:
: 自从半年前第一次用 z3 之后，现在做任何优化或者调度的任务，首先想能不能用 z3 解决。Constraints based programming 很符合偷懒的思维方式。
: #发自zSMTH@Moto Z3 Play

#发自zSMTH@Moto Z3 Play
--
FROM 188.67.236.*