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

Question

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

\n

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

\n

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

\n

使用方法很简单。就像这样——

\n

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

\n

如果以这种方式调用，结果如下所示

\n

 python test_1.py                                                                                                                                                                              \xe2\x9c\x94 \xe2\x94\x82 SAT Py \nsat\n[x3 = False, x2 = True, x1 = True, x4 = False]\n

\n

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

\n

提前致谢

\n

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，你可以这样写：

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

打印：

[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，因此当您调用时，z3 将在内部使用正确的解析器s.from_file。从命令行，您可以使用扩展.dimacs，或将命令行选项传递-dimacs给 z3。