我和我的实验室伙伴正在编写代码，为我们的一门课程使用 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)