3

我正在尝试通过其 Python 接口使用 Z3 来推断简单线性公式的可满足性。即使在我以 smt2 格式写下的以下简单公式（由 10 个子句和每个 10 个术语组成）之类的简单公式上，它似乎也很慢：

(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 84 x0)) (* 48 x1)) (* 55 x2)) (* -46 x3)) (* -8 x4)) (* -12 x5)) (* 34 x6)) (* 35 x7)) (* -36 x8)) (* 99 x9)) 77))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -66 x0)) (* -13 x1)) (* -81 x2)) (* -88 x3)) (* -42 x4)) (* 57 x5)) (* 46 x6)) (* -9 x7)) (* -39 x8)) (* 18 x9)) 4))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -18 x0)) (* 93 x1)) (* 23 x2)) (* 25 x3)) (* 63 x4)) (* 47 x5)) (* -68 x6)) (* -25 x7)) (* 49 x8)) (* 14 x9)) 78))
(assert (<= (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -44 x0)) (* -89 x1)) (* -48 x2)) (* -25 x3)) (* 40 x4)) (* 84 x5)) (* 40 x6)) (* 52 x7)) (* -8 x8)) (* 66 x9)) 5))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 30 x0)) (* 29 x1)) (* 64 x2)) (* 18 x3)) (* 63 x4)) (* -94 x5)) (* 20 x6)) (* -30 x7)) (* 60 x8)) (* -35 x9)) 72))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 97 x0)) (* -90 x1)) (* 74 x2)) (* -51 x3)) (* 70 x4)) (* 41 x5)) (* 31 x6)) (* 99 x7)) (* -34 x8)) (* 36 x9)) 60))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 38 x0)) (* -11 x1)) (* -82 x2)) (* -59 x3)) (* 93 x4)) (* 2 x5)) (* 69 x6)) (* 86 x7)) (* -83 x8)) (* 49 x9)) 14))
(assert (<= (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -55 x0)) (* 50 x1)) (* -48 x2)) (* -27 x3)) (* -7 x4)) (* 86 x5)) (* -15 x6)) (* 96 x7)) (* -46 x8)) (* 11 x9)) 56))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 50 x0)) (* -51 x1)) (* -32 x2)) (* -23 x3)) (* -75 x4)) (* 24 x5)) (* 39 x6)) (* -89 x7)) (* 8 x8)) (* 23 x9)) 36))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -50 x0)) (* 98 x1)) (* 62 x2)) (* -39 x3)) (* -90 x4)) (* 19 x5)) (* -10 x6)) (* 32 x7)) (* -51 x8)) (* 52 x9)) 24))
(check-sat)

我正在使用以下代码块动态生成这些公式：（注意：公式是子句列表；子句是术语列表、比较符号和自由系数；术语是一对变量标识符（整数)，变量的系数（整数））。

import z3
from pyCloSE.formula import LE, SAT, UNSAT, UNKNOWN

context = z3.Context()
solver = z3.SolverFor("QF_LIA", context)

# Define all variables as integers.
definitions = dict()
for variable in formula.getVariables():
    definitions[variable] = z3.Int("x{}".format(variable), context) 

# Create assertions.
constraints = []
for clause in formula.getClauses(): 
    terms = [term.getCoefficient() * definitions[term.getIndex()] for term in clause.getTerms()]
    sumOfTerms = reduce(lambda a,b: a+b, terms)

    if clause.getComparison() == LE:
        constraints.append(sumOfTerms <= clause.getFreeCoefficient())
    else:
        constraints.append(sumOfTerms != clause.getFreeCoefficient())

solver.add(*constraints)
result = solver.check()
return result

我遇到的问题是 Z3 被困在这样的公式上。当我将它保存到名为 formula.smt2 的文件并尝试通过 bash Z3 命令解决它时，它似乎也被卡住了。

我使用的求解器版本是：Z3 version 4.3.2

是我使用的格式不方便还是因为 Z3？有什么技巧可以用来加快求解过程吗？

正如胡安·奥斯皮纳建议的那样，我试图找出公式的哪一部分对求解器来说是困难的。它似乎是以下内容：

(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -18 x0)) (* 93 x1)) (* 23 x2)) (* 25 x3)) (* 63 x4)) (* 47 x5)) (* -68 x6)) (* -25 x7)) (* 49 x8)) (* 14 x9)) 78)) 
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 30 x0)) (* 29 x1)) (* 64 x2)) (* 18 x3)) (* 63 x4)) (* -94 x5)) (* 20 x6)) (* -30 x7)) (* 60 x8)) (* -35 x9)) 72)) 
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 97 x0)) (* -90 x1)) (* 74 x2)) (* -51 x3)) (* 70 x4)) (* 41 x5)) (* 31 x6)) (* 99 x7)) (* -34 x8)) (* 36 x9)) 60)) 
(assert (<= (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -55 x0)) (* 50 x1)) (* -48 x2)) (* -27 x3)) (* -7 x4)) (* 86 x5)) (* -15 x6)) (* 96 x7)) (* -46 x8)) (* 11 x9)) 56)) 
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* 50 x0)) (* -51 x1)) (* -32 x2)) (* -23 x3)) (* -75 x4)) (* 24 x5)) (* 39 x6)) (* -89 x7)) (* 8 x8)) (* 23 x9)) 36))
(assert (distinct (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ 0 (* -50 x0)) (* 98 x1)) (* 62 x2)) (* -39 x3)) (* -90 x4)) (* 19 x5)) (* -10 x6)) (* 32 x7)) (* -51 x8)) (* 52 x9)) 24))

事实上，如果你从这个公式中删除任何子句，求解器能够在不到一秒钟的时间内回答，而如果你用整个公式来输入它，它就会超时。

为什么会这样？Z3觉得这个公式这么难解是正常的吗？

最好的，安德里亚

4

0 回答 0