我有两个 SMT 问题实例。第一个在这里:
http://gist.github.com/1232766
Z3 在我不太好的机器上大约 2 分钟后返回了一个模型,这很棒。我也有这个:
http://gist.github.com/1232769
我已经在这个问题上运行了 z3 一夜之间,没有 Z3 完成。如果您检查这些文件的内容,您会发现第二个与第一个相同,只是它有一个额外的断言来“拒绝”第一个实例返回的模型。(你可以在它们之间做一个“差异”来了解我的意思。)我碰巧知道这个问题有多个令人满意的模型,我正在尝试使用 z3 来找到所有令人满意的模型。
我知道这可能完全在意料之中,但我很想知道为什么与第一个相比,第二个对 Z3 来说是一个更棘手的问题。有没有更好的方法来制定第二个问题,这样 Z3 会更轻松?
谢谢..