随机可满足性模理论
Stochastic Satisfiability Modulo Theory
有人知道 Z3 是否支持 SSMT（即随机量词）或者是否有任何计划添加它？
目前没有直接处理随机量词的计划。
那篇论文的作者可能有更多的信息。论文指向一个系统：https://projects.avacs.org/projects/sisat/wiki/SiSAT_Manual
但是，过去 3 年它一直处于非活动状态，所以我不确定这是否
是作者迫切追求的东西。也许有后续系统。
我正在考虑的最接近的是交替 min/max objectives。也就是说，您应该能够计算一些 objective 函数 f(x,y)，这样 x, y
满足约束 Phi(x,y) 并服从 min x max y f(x,y)。
后者意味着找到 x，使得 f(x,y) 在所有 y 上最小化。
在 Z3 的顶部（而非内部）实施 SSMT（和类似）的工作正在进行（但目前很低 activity），这在某些特定问题上优于 Tino Teige 的方法和 Prism，请参阅here and here.
有人知道 Z3 是否支持 SSMT（即随机量词）或者是否有任何计划添加它？
目前没有直接处理随机量词的计划。 那篇论文的作者可能有更多的信息。论文指向一个系统：https://projects.avacs.org/projects/sisat/wiki/SiSAT_Manual 但是，过去 3 年它一直处于非活动状态，所以我不确定这是否 是作者迫切追求的东西。也许有后续系统。 我正在考虑的最接近的是交替 min/max objectives。也就是说，您应该能够计算一些 objective 函数 f(x,y)，这样 x, y 满足约束 Phi(x,y) 并服从 min x max y f(x,y)。 后者意味着找到 x，使得 f(x,y) 在所有 y 上最小化。
在 Z3 的顶部（而非内部）实施 SSMT（和类似）的工作正在进行（但目前很低 activity），这在某些特定问题上优于 Tino Teige 的方法和 Prism，请参阅here and here.