z3 - Z3 返回未知

Question

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

http://pastebin.com/3eaLQ9wx

有没有办法调整约束以获得结果？这是一组更大的约束（数千个）的一个简单示例，但我不知何故感到困扰，即使在这样简单的示例上它也不起作用

提前致谢 ！！

Answer 1

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

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