sat-solvers - SAT 求解器，0 深度作业

Question

在谈论 SAT 求解器时，例如 minisat，“0-depth”和“CNF assignments”的值是什么意思？这些值通常是各种 SAT 求解器信息输出的一部分。

Answer 1

零深度分配是在 DPLL 搜索开始之前设置变量的值。MiniSAT对公式做的预处理（包含、自包含等）有时可以证明一个变量一定有一定的值。如果可以，MiniSAT 将在开始 DPLL 程序之前修复这些变量的值。