在Z3中使用quantifer消除Python

我嘗試使用solve(g)來找到滿足公式g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0)))的A，B，C，D的值。這有很多可能的解決方案，一個是A=1,B=-1,C=D=0但Z3似乎無法做到這一點（solve(g)不會終止）。在Z3中使用quantifer消除Python

Z3可以做這種非線性（但簡單）的公式嗎？也許我可以指定一些量化寬鬆策略或其他什麼？

來源

2013-02-19 Vu Nguyen

Z3有一個量詞消除策略。我們可以通過創建使用解算器啓用：

s = Then('qe', 'smt').solver()

此命令將創建第一應用量詞消去，然後調用SMT求解求解器。但是，Z3對非線性公式的量詞消除的支持非常有限。你的例子是非線性的，因爲它包含：A * i + B * j + C * k + D <= 0。因此，qe策略將無法消除量詞。

如果您可以對非線性算法實現更好的QE支持，那將會很棒。

來源

2013-02-19 02:08:07

感謝萊昂納多，如果不支持非線性算術的QE，那麼爲什麼不只是在求解這些公式時求解（g）'返回未知或不支持？相反，它似乎是在試圖做點什麼？另外，Z3是否支持非線性*等值*或任何其他非線性算術類？你知道其他SMT解算器是否提供對非線性算術的支持嗎？再次感謝 – 2013-02-19 05:34:28

Z3使用啓發式實例化和基於模型的量詞實例化。這些方法不完整，但可以解決許多問題。請注意，發送給Z3的大多數問題（包含量詞）都是不可判定的片段，但這並不妨礙Z3解決其中的一部分問題。 – 2013-02-19 16:19:05

據我所知，Z3對非線性算法有最好的支持。（非量詞）非線性算術問題非常有效。請參閱本文末尾的比較http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf – 2013-02-19 16:20:52

在Z3中使用quantifer消除Python

回答

相關問題