1

我创建了大约 20k 个约束，在我的机器上解决它们大约需要 3 分钟。我有不同类型的约束，下面我给出例子并解释它们。我将断言上传到http://filebin.ca/vKcV1gvuGG3。

我对解决更大的约束系统很感兴趣，因此我想加快这个过程。我想问一下您是否有关于如何更快地解决它们的建议，例如通过使用适当的策略。从关于策略的教程中，我知道了策略，但我似乎没有通过应用策略获得积极的差异......

li是树的标签。第一种类型对标签的值进行了限制。标签值通常介于 10-20 个不同的值之间。

Or(l6 == 11, Or(l6 == 0, l6 == 1, l6 == 2, l6 == 3, l6 == 4,
      l6 == 5, l6 == 6, l6 == 7, l6 == 8, l6 == 9, l6 == 10))

第二种类型将不同的标签相互关联。

Implies(l12 == 0, Or(l10 == 2, l10 == 5, l10 == 7, l10 == 8, l10 == 10,
           False, False))

第 3 种类型定义和关联函数f: Int --> Int（或f: BitVector --> BitVector，不完整），其中bound_{s, v}只是函数名称，n是节点的 ID。目标是找到令人满意的功能分配bound。

Implies(And(bound_s_v (18) >= 0, l18 == 0),
        And(bound_s_v (19) >= 0,
            bound_s_v (19) >=
            bound_s_v (18),
            bound_s_v (26) >= 0,
            bound_s_v (26) >=
            bound_s_v (18)))

最后一种类型确定是否需要边界 ( >= 0) 或不需要 ( == -1, )

Or(bound_s'_v'(0) >= 0, bound_s'_v'(0) == -1)

还有一个要求，对于某些初始状态，边界是必需的：

`bound_s0_v0(0) >= 0`

可执行文件的描述：在前 2-3 行中，脚本启动求解器，导入 z3 并在最后一行调用print s.check()

4

1 回答 1

0

大概，您可以尝试使用求解器“qflia”，因为我在您的逻辑中看不到量词。

编辑：

我试过'qflia'，但它并没有让它更快。也许，您也应该尝试其他求解器。

于 2015-08-11T19:58:37.183 回答