python-3.xdeprecation-warningcnf

Warning in script running minisat: difficult to understand


Good day, I'm running a python script on Linux about a graph of connections that are to be coloured in 2 different colours so that no two same colours are connected. The script is to return an answer in CNF format using minisat such as 'SATISFIABLE' OR 'UNSATISFIABLE', nothing more. However, even tho I've gotten my script to work perfectly and it passes all the tests I had, it keeps throwing two warnings at me Warning: for repeatability, setting FPU to use double precision. Warning! DIMACS header mismatch: wrong number of variables. I have never gotten these warnings before and can't find anything about them anywhere.

# python3

import itertools
import os
from subprocess import DEVNULL, STDOUT, check_call, call
import warnings

warnings.filterwarnings(action = "ignore", message = 'for repeatability, setting FPU to use double precision')

n, m = map(int, input().split())
edges = [list(map(int, input().split())) for i in range(m)]

clauses = []
colors = range(1, 4)

def varnum(i, k):
    assert(i in colors and k in colors)
    return 3 * (i - 1) + k

def exactlyOneOf(i):
    literal = [varnum(i, k) for k in colors]
    clauses.append([l for l in literal])
    for pair in itertools.combinations(literal, 2):
        clauses.append([-l for l in pair])

def adj(i, j):
    for k in colors:
        clauses.append([-varnum(i, k), -varnum(j, k)])

for i in range(1, n + 1):
    exactlyOneOf(i)

for i, j in edges:
    adj(i, j)

#print(len(clauses)) #, n * 3)
#for c in clauses:
 #   c.append(0)
  #  print(' '.join(map(str, c)))

with open('tmp.cnf', 'w') as f:
    f.write('p cnf {} {}\n'.format(999, len(clauses)))
    for c in clauses:
        c.append(0)
        f.write(" ".join(map(str, c)) + "\n")

os.system("minisat -verb=0 tmp.cnf tmp.sat")
call(['minisat', 'tmp.cnf', 'tmp.sat'], stdout = DEVNULL, stderr = STDOUT)

with open("tmp.sat", "r") as satfile:
    for line in satfile:
        if line.split()[0] == "UNSAT":
            print("There is no solution")
        elif line.split()[0] == "SAT":
            #print("SATISFIABLE")
            pass
        else:
            assignment = [int(x) for x in line.split()]
            for i in colors:
                for k in colors:
                    if varnum(i, k) in assignment:
                        #print(k)
                        break
                #print("")


Solution

  • I don't know how I did it but I got rid of the warning by using the subprocess module to call Minisat instead of using the OS module. I initially tried to use a call from the subprocess module but kept getting an error so I tweaked my code a bit and finally got rid of the error using this code line.

    subprocess.call(['minisat', 'tmp.cnf', 'tmp.sat'], stdout = subprocess.DEVNULL, stderr = subprocess.STDOUT)