我和我的实验室伙伴正在编写代码，为我们的一门课程使用 Python 制作我们自己的 SAT 求解器。到目前为止，我们已经编写了将 SoP 转换为 CNF 的代码。现在我们陷入如何将 CNF 转换为 DIMACS 格式的问题。我们了解 DIMACS 格式在手动完成时的工作原理，但我们仍坚持编写从 CNF 到 DIMACS 的实际代码。到目前为止我们发现的所有输入文件都已经是 DIMACS 格式。
from sympy.logic.boolalg import to_cnf
from sympy.abc import A, B, C, D
f = to_cnf(~(A | B) | D)
g = to_cnf(~A&B&C | ~D&A)
sympy boolalg 模块可让您为表达式构建抽象语法树 (AST)。在 CNF 形式中，您将有一个顶级And节点，带有一个或多个子节点；每个子节点都是一个Or具有一个或多个文字的节点；文字要么是Not符号的节点，要么直接是符号。
从DIMACS方面来看，顶层And是隐式的。您只是列出Or节点，如果符号位于 a 中，则在符号的变量之前Not用 标记它。-您本质上只是为符号指定新名称并以新的文本形式写下来。（事实上，DIMACS 变量名称看起来像整数只是因为它很方便；它们没有整数语义/算术/等。）
要跟踪 DIMACS 变量和 sympy 符号之间的映射，类似这样的操作会很有帮助：
\nclass DimacsMapping:\n def __init__(self):\n self._symbol_to_variable = {}\n self._variable_to_symbol = {}\n self._total_variables = 0\n\n @property\n def total_variables(self):\n return self._total_variables\n\n def new_variable(self):\n self._total_variables += 1\n return self._total_variables\n\n def get_variable_for(self, symbol):\n result = self._symbol_to_variable.get(symbol)\n if result is None:\n result = self.new_variable()\n self._symbol_to_variable[symbol] = result\n self._variable_to_symbol[result] = symbol\n\n return result\n\n def get_symbol_for(self, variable):\n return self._variable_to_symbol[variable]\n\n def __str__(self) -> str:\n return str(self._variable_to_symbol)\n您始终可以使用 请求一个新的（新鲜的，从未使用过的）变量new_variable。DIMACS 变量从 1 开始，而不是 0。（0 值用于指示非变量，主要用于标记子句结束。）
我们不想每次都分配新变量，但还要记住哪些变量被分配给了符号。这维护了从符号到变量的映射，反之亦然。您传递一个 sympy 符号get_variable_for，然后返回该符号之前使用的变量，或者分配并返回一个新变量，并记录映射。
get_symbol_for它跟踪反向映射，因此您可以根据;中给定的变量恢复原始符号。这对于将 SAT 作业转回 sympy 作业非常有用。
接下来，我们需要一些东西来存储这个映射以及子句列表。您需要两者都发出有效的 DIMACS，因为标题行包含变量计数（映射知道）和子句计数（子句列表知道）。这基本上是一个美化的元组，其中的 a__str__可以转换为格式良好的 DIMACS 文本：
class DimacsFormula:\n def __init__(self, mapping, clauses):\n self._mapping = mapping\n self._clauses = clauses\n\n @property\n def mapping(self):\n return self._mapping\n\n @property\n def clauses(self):\n return self._clauses\n\n def __str__(self):\n header = f"p cnf {self._mapping.total_variables} {len(self._clauses)}"\n body = "\\n".join(\n " ".join([str(literal) for literal in clause] + ["0"])\n for clause in self._clauses\n )\n\n return "\\n".join([header, body])\n最后，我们只需遍历 sympy AST 来创建 DIMACS 子句：
\nfrom sympy.core.symbol import Symbol\nfrom sympy.logic.boolalg import to_cnf, And, Or, Not\n\ndef to_dimacs_formula(sympy_cnf):\n dimacs_mapping = DimacsMapping()\n dimacs_clauses = []\n\n assert type(sympy_cnf) == And\n for sympy_clause in sympy_cnf.args:\n assert type(sympy_clause) == Or\n\n dimacs_clause = []\n for sympy_literal in sympy_clause.args:\n if type(sympy_literal) == Not:\n sympy_symbol, polarity = sympy_literal.args[0], -1\n elif type(sympy_literal) == Symbol:\n sympy_symbol, polarity = sympy_literal, 1\n else:\n raise AssertionError("invalid cnf")\n\n dimacs_variable = dimacs_mapping.get_variable_for(sympy_symbol)\n dimacs_literal = dimacs_variable * polarity\n dimacs_clause.append(dimacs_literal)\n\n dimacs_clauses.append(dimacs_clause)\n\n return DimacsFormula(dimacs_mapping, dimacs_clauses)\n这只是沿着树下降，直到它得到根符号以及它是否被否定（即，处于指示Not负极性）。一旦符号被映射到它的变量，我们就可以将其保留为正或取反以保持极性并将其附加到 DIMACS 子句中。
对所有Or节点执行此操作，我们就有了映射的 DIMACS 公式。
f = to_cnf(~(A | B) | D)\nprint(f)\nprint()\n\nf_dimacs = to_dimacs_formula(f)\nprint(f_dimacs)\nprint()\nprint(f_dimacs.mapping)\n(D | ~A) & (D | ~B)\n\np cnf 3 2\n1 -2 0\n1 -3 0\n\n{1: D, 2: A, 3: B}\n顺便说一句，您可能不想使用to_cnf获取 CNF 来测试可满足性。一般来说，将布尔公式转换为等效的 CNF 可能会导致大小呈指数增长。
请注意，在上面的示例中f，变量D在公式中仅出现一次，但在 CNF 中出现两次。如果它更复杂，比如(C | D)，那么整个子公式都会被复制：
f = to_cnf(~(A | B) | (C | D))\nprint(f)\n(C | D | ~A) & (C | D | ~B)\n如果更复杂，您可以看到如何最终得到副本的副本的副本......等等。为了测试可满足性，我们不需要等价公式，而只需要一个可等满足的公式。
\n这是一个可能不等价的公式，但当且仅当原始公式是等价的时才是可满足的。它可以有新的子句和不同的变量。这种松弛反而给出了线性大小的平移。
\n为此，我们将分配一个代表该子公式真值的变量并使用它，而不是允许复制子公式。这称为Tseitin 变换，我将在这个答案中详细介绍。
\n作为一个简单的例子，假设我们想使用一个变量x来表示(a \xe2\x88\xa7 b)。我们将其写为x \xe2\x89\xa1 (a \xe2\x88\xa7 b)，这可以通过三个 CNF 子句来完成：(\xc2\xacx \xe2\x88\xa8 a) \xe2\x88\xa7 (\xc2\xacx \xe2\x88\xa8 b) \xe2\x88\xa7 (\xc2\xaca \xe2\x88\xa8 \xc2\xacb \xe2\x88\xa8 x)。x当且仅当是时，现在才是正确的(a \xe2\x88\xa7 b)。
该顶级函数启动该过程，以便递归调用共享相同的映射和子句集。最终结果是代表整个公式的真值的单个变量。我们必须强制这是真的（否则 SAT 求解器将简单地选择公式的任何输入变量，遵循含义，并生成任何输出的评估公式）。
\ndef to_dimacs_tseitin(sympy_formula):\n dimacs_mapping = DimacsMapping()\n dimacs_clauses = []\n\n # Convert the formula, with this final variable representing the outcome\n # of the entire formula. Since we are stating this formula should evaluate\n # to true, this variable is appended as a unit clause stating such.\n formula_literal = _to_dimacs_tseitin_literal(\n sympy_formula, dimacs_mapping, dimacs_clauses\n )\n dimacs_clauses.append([formula_literal])\n\n return DimacsFormula(dimacs_mapping, dimacs_clauses)\n大部分翻译是添加特定于正在执行的操作的子句的代码。递归发生在我们需要一个代表子公式参数的输出的变量时。
\ndef _to_dimacs_tseitin_literal(sympy_formula, dimacs_mapping, dimacs_clauses):\n # Base case, the formula is just a symbol.\n if type(sympy_formula) == Symbol:\n return dimacs_mapping.get_variable_for(sympy_formula)\n\n # Otherwise, it is some operation on one or more subformulas. First we\n # need to get a literal representing the outcome of each of those.\n args_literals = [\n _to_dimacs_tseitin_literal(arg, dimacs_mapping, dimacs_clauses)\n for arg in sympy_formula.args\n ]\n\n # As a special case, we won\'t bother wasting a new variable for `Not`.\n if type(sympy_formula) == Not:\n return -args_literals[0]\n\n # General case requires a new variable and new clauses.\n result = dimacs_mapping.new_variable()\n\n if type(sympy_formula) == And:\n for arg_literal in args_literals:\n dimacs_clauses.append([-result, arg_literal])\n dimacs_clauses.append(\n [result] + [-arg_literal for arg_literal in args_literals]\n )\n elif type(sympy_formula) == Or:\n for arg_literal in args_literals:\n dimacs_clauses.append([result, -arg_literal])\n dimacs_clauses.append(\n [-result] + [arg_literal for arg_literal in args_literals]\n )\n else:\n # TODO: Handle all the other sympy operation types.\n raise NotImplementedError()\n\n return result\n现在布尔公式不需要在 CNF 中即可成为 DIMACS：
\nf = ~(A | B) | (C | D)\nprint(f)\nprint()\n\nf_dimacs = to_dimacs_tseitin(f)\nprint(f_dimacs)\nprint()\nprint(f_dimacs.mapping)\nC | D | ~(A | B)\n\np cnf 6 8\n5 -3 0\n5 -4 0\n-5 3 4 0\n6 -1 0\n6 -2 0\n6 5 0\n-6 1 2 -5 0\n6 0\n\n{1: C, 2: D, 3: A, 4: B}\n即使在单位传播之后，在这个小例子中得到的公式也明显更大。然而，当转换“真实”公式时，线性缩放有很大帮助。此外，现代 SAT 求解器了解公式将以这种方式进行转换，并执行针对其量身定制的处理中操作。
\n