How to solve a 2-SAT instance with 60 boolean variables and 99 clauses using Z3Py

Question

I am using the following code:

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

The output is: run this example online here

In this example the matrix M defines the 2-SAT instance as a CNF (reference). In this example the matrix M was introduced as an input by hand. Please let me know how to introduce the matrix M automatically (matrix). Many thanks.

Answer 1

-- My question: how to read the matrix M from an archive txt using Z3Py

I am afraid I can only give a very general answer to this question. The general answer is to write a parser in python and feed the result to the interface functions exposed over Z3py. There are many examples online of writing parsers for various formats, including the DIMACS format.

Z3 exposes some APIs for parsing benchmarks in the SMT-LIB2 format. You can call these API functions from Python. The relevant functions in the Python wrapper are called parse_smt2_string and parse_smt2_file.