z3 - Z3 Python API は線形数式で遅いようです

Question

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 バージョン 4.3.2

使用しているフォーマットが不便ですか、それとも Z3 のせいですか? 解決プロセスをスピードアップするために使用できるトリックはありますか?

Juan Ospina が提案したように、数式のどの部分がソルバーにとって難しい部分であるかを把握しようとしました。以下のようです。

(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))

実際、この式から任意の句を削除すると、ソルバーは 1 秒以内に応答できますが、式全体を入力すると時間切れになります。

なぜこれが起こるのですか？Z3がこの式を解くのがとても難しいと思うのは普通ですか?

ベスト、アンドレア