Z3返回未知

Question

我有一組簡單的約束Z3是無法應付的：

http://pastebin.com/3eaLQ9wx

是否有辦法來調整，以獲得結果的約束？ 這是一個較大的約束（千）的一個簡單的例子，但 我有點困擾，即使在這樣簡單的例子，它不起作用

在此先感謝！

Answer 1

您的問題有非線性約束。雖然Z3在大多數情況下可以處理它們，但是Int s和Real的混合似乎超出了目前的能力。如果您只是使用Real s爲您的s_0_1,s_0_2等變量，我相信Z3將能夠解決問題。 （你似乎有足夠的價值限制，所以我相信不存在建模問題。）

我認爲萊昂納多多次表示即將發佈的版本將會更好地支持組合理論在非線性限制。