这是我的问题。我有太多的限制。因此，生成的未饱和核心没有提供信息。但是，我手动开始排除约束，并将一组有问题的约束归零。我的目标是检查 Z3 可能存在的已知问题。我正在计算真实变量的概率p。我对他们施加界限
p1<= 1.0
p1>= 0.0
p2<= 1.0
p2>= 0.0
有一个计算概率的约束。
a=1 and b=0 implies p1 = c * p2
c这是一个常数。a,b是实变量。
现在，我观察到的是，我得到了一个 UNSAT，但去掉了界限，我得到了一个 SAT。奇怪的是，当我遍历模型时，对 p1 和 p2 的分配介于 0 和 1 之间。准确地说是 1，因此不会违反这些界限。有没有类似的已知问题？我知道这太含糊了，但是如果不将整个项目放在这里，我不确定如何提出这个问题...