Z3 返回未知答案

【问题标题】：Z3 returns unknownZ3 返回未知
【发布时间】：2012-12-31 01:36:00
【问题描述】：

我有一组 Z3 无法应对的简单约束：

有没有办法调整约束以获得结果？这是一组更大的约束（数千个）的简单示例，但是即使在这样简单的示例上也无法正常工作，我感到有些困扰

提前致谢！！

【问题讨论】：

标签： z3 smt

【解决方案1】：

您的问题具有非线性约束。虽然 Z3 在大多数情况下都可以处理它们，但 Ints 和 Real 的混合似乎超出了它目前的能力。如果您只是将Reals 用于您的s_0_1、s_0_2 等变量，我相信Z3 将能够解决问题。（你似乎有足够的价值约束，所以我相信不会有建模问题。）

我认为莱昂纳多多次表示，即将发布的版本将更好地支持存在非线性约束的组合理论。

【讨论】：

Levent 是正确的，问题是使用混合整数和实数非线性算术。我看到了两种可能的解决方法。我们可以用实变量替换所有整数变量，这没关系，因为整数变量在您的问题中只能假设 0 或 1 值（这里是这个解决方案：rise4fun.com/Z3Py/ICFA）。在这种情况下，将使用 Z3 中的新 nlsat 求解器。另一种选择是将整数变量替换为布尔变量，并使用Ifs 将问题线性化。这是此解决方案的链接rise4fun.com/Z3Py/egCe。第二种解决方案应该可以更好地扩展。