Linux下Python调用MiniSAT出现两类警告的技术求助

1. 关于FPU精度设置的警告 #

你用Python的warnings模块尝试忽略这个警告，但这个警告是MiniSAT程序本身输出的，不属于Python警告体系，所以Python的过滤规则无效。另外代码里重复调用了两次MiniSAT：一次用os.system（未重定向错误输出），一次用subprocess.call（已重定向输出），前者是警告弹出的原因。

修复方法：

• 删除os.system("minisat -verb=0 tmp.cnf tmp.sat")这一行，只保留subprocess.call的调用，它已经把标准输出和错误输出都重定向到了DEVNULL，不会显示警告。

2. DIMACS头变量数不匹配的警告 #

你的CNF文件头里变量数写死成了999，但实际变量数应该是所有节点对应的颜色变量总数：每个节点有3个颜色变量（对应colors = range(1,4)），n个节点的总变量数是3 * n。MiniSAT会校验头文件声明的变量数和实际出现的最大变量值，不匹配就会弹出警告。

修复方法：

• 计算正确的变量数，修改CNF头的写法：

  f.write('p cnf {} {}\n'.format(3 * n, len(clauses)))
  

修改后的完整代码 #

# python3

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

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 range(1, n+1) and k in colors)  # 修正断言逻辑，i是节点编号而非颜色
    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)

with open('tmp.cnf', 'w') as f:
    f.write('p cnf {} {}\n'.format(3 * n, len(clauses)))  # 修正变量数声明
    for c in clauses:
        c.append(0)
        f.write(" ".join(map(str, c)) + "\n")

# 仅保留一次MiniSAT调用，且重定向所有输出
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":
            pass
        else:
            assignment = [int(x) for x in line.split()]
            for i in range(1, n+1):  # 修正循环范围，遍历所有节点而非颜色
                for k in colors:
                    if varnum(i, k) in assignment:
                        # print(k)
                        break
                # print("")

额外修正了两处逻辑小问题：varnum函数的断言逻辑（原断言把节点编号和颜色范围搞混）、最后遍历节点的循环范围（原循环错误遍历了颜色列表）。

内容的提问来源于stack exchange，提问作者Omolewa Oreweme