Как решить экземпляр 2-SAT с 60 логическими переменными и 99 предложениями, используя Z3Py

Question

Я использую следующий код:

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 ( ссылка). В этом примере матрица М была введена в качестве ввода вручную. Пожалуйста, дайте мне знать, как ввести матрицу М автоматически ( матрица). Большое спасибо.

Answer 1

- мой вопрос: как прочитать матрицу M из архива txt с помощью Z3Py

Боюсь, я могу дать только очень общий ответ на этот вопрос. Общий ответ - написать синтаксический анализатор на python и передать результат интерфейсным функциям, предоставляемым через Z3py. В Интернете есть много примеров написания синтаксических анализаторов для различных форматов, включая формат DIMACS.

Z3 предоставляет некоторые API для анализа тестов в формате SMT-LIB2. Вы можете вызвать эти функции API из Python. Соответствующие функции в оболочке Python называются parse_smt2_string и parse_smt2_file.