QF_AUFBV实例有一个难以置信的困难假设

从Z3py转储的smt2代码是here。如果您向下滚动到底部，您会看到有一个假设，如果发表评论，则会立即使问题得以解决。QF_AUFBV实例有一个难以置信的困难假设

我有几个问题：

我有没有选择正确的理论，QF_AUFBV？
为什么这个假设让实例变得更加困难？
任何线索如何去调试它呢？

我已经解决了类似的情况，它们相当快。

当我解决这个问题，从Z3py具有详细= 10，我看到这样的输出，而这是解决：如果

(smt.restarting :propagations 35577 :decisions 13935 :conflicts 277 :restart 110 :restart-outer 110 :agility 0.0356467) 
(smt.restarting :propagations 40109 :decisions 15040 :conflicts 388 :restart 100 :restart-outer 121 :agility 0.0452989) 
(smt.restarting :propagations 43945 :decisions 15901 :conflicts 489 :restart 110 :restart-outer 121 :agility 0.0671191)

不知道这是有帮助的。谢谢。

来源

2015-05-07 EfForEffort

输入中的小改变通常会对Z3s运行时产生巨大影响，特别是如果它们不连贯（就像您的假设）。看起来在这个问题上，SMT核心求解器简单地陷入了搜索解决方案的困境，在尝试了数千个分支（:decisions 13935）之后，它决定放弃并从头开始（smt.restarting...）。

理论选择很好。如果你不需要UF，你可以将它设置为QF_ABV，但默认情况下，Z3将使用相同的战术/参数。

我不知道我看到哪里有一个“调试”的错误，但我想通过“调试”你的意思是“让它变得更快”？

来源

2015-05-08 18:24:15

我知道求解时间从求解器到求解器有时是不一样的（有时是疯狂的），但是Boolector能够立即解决这个例子。我想我想知道是否有一些我可以尝试的相关策略，或者替代编码，或者我可以设置的一些我不知道的解算参数。谢谢参观。 – EfForEffort

QF_AUFBV实例有一个难以置信的困难假设

回答

相关问题