为 Z3 读取和解析 DIMACS 的更好方法

Question

我对 SAT 和 Z3 非常陌生（甚至还没有开始接触 SMT）。我一直在玩gophersat（一个很好的 Go 实现，适用于一组很好的 SAT 问题），我在那里发现了 DIMACS 格式。虽然我同意这不是使用变量的最佳方式，但对于一些简单的测试，我发现它非常方便。我试图检查是否有直接的方法可以从 Z3 中的 DIMACS 文件中读取、解析和构造 SAT 公式。我没有找到任何（如前所述，我很新，所以我可能不知道存在一个）。所以我最终编写了以下代码。我想知道人们对此有何看法以及是否有更好的方法来实现这一目标。

（注意：我没有对公式的子句数量和/或变量数量进行任何检查）

from z3 import *


def read_dimacs_and_make_SAT_formula(file_name: str):
    vars = dict()
    base_name = "x"
    with open(file_name, "r") as f:
        for idx, line in enumerate(f):
            if line.strip() != "\n" and line.strip() != "" and line.strip() != "\r" and line.strip() != None and idx > 0:
                splitted_vals = line.split()
                for element in splitted_vals:
                    if int(element) != 0:
                        if int(element) > 0 and vars.get(element) is None:
                            # pure variable which never seen
                            vars[element] = Bool(base_name+element)
                        elif int(element) > 0 and vars.get("-"+element) is not None:
                            # pure variable we have seen the negetion before.
                            vars[element] = Not(vars["-"+element])
                        elif int(element) < 0 and vars.get("-"+element) is None:
                            # negetion of a variable and we have not seen it before.
                            vars[element] = Not(Bool(base_name+element.replace("-", "")))
                        elif int(element) < 0 and vars.get(element.replace("-", "")) is not None:
                            # Negetion, we have seen the pure variable before.
                            vars[element] = Not(vars[element.replace("-", "")])
        f.seek(0)
        disjunctions = []
        for idx, line in enumerate(f):
            clauses = []
            if line.strip() != "\n" and line.strip() != "" and line.strip() != "\r" and line.strip() != None and idx > 0:
                splitted_vals = line.split()
                for element in splitted_vals:
                    if int(element) != 0:
                        clauses.append(vars[element])
                disjunctions.append(Or([*clauses]))
        # print(disjunctions)
        if disjunctions:
            return And([*disjunctions])
        return None

您使用它的方式很简单。像这样-

if __name__== "__main__":
    s = Solver()

    disjunctions = read_dimacs_and_make_SAT_formula("dimacs_files/empty.cnf")
    if disjunctions is not None:
        s.add(disjunctions)
        print(s.check())
        if s.check().r != -1:
            print(s.model())

如果这样调用，结果如下所示

 python test_1.py                                                                                                                                                                              ✔ │ SAT Py 
sat
[x3 = False, x2 = True, x1 = True, x4 = False]

所以问题是，你怎么看？我可以做点别的吗？有没有更好的办法？

提前致谢

Answer 1

请注意，代码审查通常与堆栈溢出无关。有一个专门的堆栈交换网站 (https://codereview.stackexchange.com) 用于此类目的。您可能会在那里获得有关您的计划的更好反馈。

话虽如此，z3 开箱即用地支持 DIMACS 格式，因此您实际上不需要对其进行编程。这是一个例子。假设我们有文件a.dimacs：

c  simple_v3_c2.cnf
c
p cnf 3 2
1 -3 0
2 3 -1 0

你可以直接把这个喂给z3：

$ z3 a.dimacs
s SATISFIABLE
v -1 -2 -3

或者，如果你想使用 Python API，你可以这样写：

from z3 import *

s = Solver()
s.from_file("a.dimacs")
print(s)
print(s.check())
print(s.model())

哪个打印：

[Or(k!1, Not(k!3)), Or(Not(k!1), k!2, k!3)]
sat
[k!1 = False, k!3 = False, k!2 = False]

请注意，文件扩展名必须为dimacs，因此当您调用s.from_file 时，z3 将在内部使用正确的解析器。在命令行中，您可以使用 .dimacs 扩展名，或将命令行选项 -dimacs 传递给 z3。