z3 - Z3 が不明を返す

Question

Z3 が対処できない単純な一連の制約があります。

http://pastebin.com/3eaLQ9wx

結果を得るために制約を微調整する方法はありますか? これはより大きな制約セット (数千) の単純な例ですが、このような単純な例でも機能しないことに何となく困っています。

前もって感謝します ！！

Answer 1

問題には非線形制約があります。Z3 はほとんどの場合それらを処理できますが、 と が混在しIntてRealいるため、現在の機能を超えているようです。などの変数に単にReals を使用する場合、Z3 が問題を解決できると信じています。(十分な値の制約があるようですので、モデリングの問題はないと思います。)s_0_1s_0_2

レオナルドは、今後のリリースでは、非線形制約が存在する場合に結合された理論をより適切にサポートするだろうと何度か表明したと思います。