python - 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。