Как решить пример 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 

Выход: запустить этот пример онлайн here

В этом примере матрица M определяет экземпляр 2-SAT как CNF (reference). В этом примере матрица M была введена вручную. Пожалуйста, дайте мне знать, как ввести матрицу M автоматически (matrix). Большое спасибо.

Answer 1

- Мой вопрос: как читать матрицу М из архива TXT, используя Z3Py

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

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