0

次のコードを使用しています。

X = BoolVector('x', 60)
M = [[21, 34],[-49, -12],[7, 18],
     [-5, -1],[28, 17],
     [3, 55],[36, 33],
     [-6, -50],[44, -41],
     [-55, 3],[14, -54],[-30, 13],
     [-13, 60],[54, -16],[-48, 41],
     [3, 6],[49, -48],[34, -4],
     [14, -46],[58, -20],
     [52, 54],[-37, -25],[56, -1],
     [50, -9],[-58, 11],
     [-19, 58],[17, 8],[56, 51],
     [38, 49],[-13, 36],
     [24, 9],[18, -29],
     [6, 49],[-30, 4],[-13, -20],
     [31, -9],[54, -4],[37, 17],
     [-48, -8],[-7, -45],[-3, -42],
     [27, -22],[-50, -27],[47, 19],[-21, 20],[-20, -37],
     [-42, 12],[-35, 1],[-41, -19],[11, 30],[-17, -48],
     [21, -49],[16, -53],[57, 57],[15, 2],[-6, -7],[-23, -28],
     [-12, -17],[-59, -36],[38, -6],[-16, -6],[21, -14],
     [17, -7],[3, -49],[-55, -13],[22, -52],[24, -56],[22, -42],
     [13, -4],[-8, -16],[-55, -7],[-12, 48],
     [52, 18],[-47, 44],[-22, -23],[-29, -23],[-53, 57],
     [-38, 54],[43, -53],[49, -18],[-60, 58],[-5, -14],[16, 34],
     [-24, -43],[10, -21],[-52, -40],[-45, -22],[-5, -11],
     [-32, -11],[-15, 11],[-24, 44],[-17, -15],[10, -27],
     [8, -26],[-36, 24],[13, 1],[59, -34],[-40, -25],[11, -22]] 
     s = Solver()
     for i in range(99):
           if M[i][0] > 0:
              if M[i][1] >0:
                  s.add(Or(X[M[i][0]-1],X[M[i][2]-1]))
              else:
                  s.add(Or(X[M[i][0]-1],Not(X[-M[i][3]-1])))
           else:
              if M[i][4] >0:
                  s.add(Or(Not(X[-M[i][0]-1]),X[M[i][5]-1]))
              else:
                  s.add(Or(Not(X[-M[i][0]-1]),Not(X[-M[i][6]-1])))
print "instance 2-SAT =", s  
print s.check() 
m = s.model()     

for k in range(60):
    if is_true(m.evaluate(X[k])):
        print X[k], "=", 1
    else:
        print X[k], "=", 0

出力は次のとおりです。この例をここでオンラインで実行します

この例では、行列 M は 2-SAT インスタンスを CNF (参照) として定義します。この例では、行列 M が手動で入力として導入されました。行列 M を自動的に導入する方法を教えてください ( matrix )。どうもありがとう。

4

1 に答える 1

3

-- 私の質問: Z3Py を使用してアーカイブ txt から行列 M を読み取る方法

申し訳ありませんが、この質問には非常に一般的な回答しかできません。一般的な答えは、Python でパーサーを作成し、その結果を Z3py で公開されているインターフェイス関数に渡すことです。DIMACS 形式を含む、さまざまな形式のパーサーを作成するオンラインの例が多数あります。

Z3 は、SMT-LIB2 形式でベンチマークを解析するためのいくつかの API を公開しています。これらの API 関数は Python から呼び出すことができます。Python ラッパー内の関連する関数は、parse_smt2_string および parse_smt2_file と呼ばれます。

于 2013-08-01T20:11:40.990 に答える