支配规则的力量

当SAT求解器决定一个CNF $\Gamma$是不可 satisfiable时，标准做法是以某种证明系统中对$\Gamma$的否证形式呈现不可 satisfiability的证书。通常使用的系统是DRAT，它等价于扩展解析 (ER)——例如，直到今年DRAT否证在年度SAT竞赛中都是必需的。最近[BoGaerts等人，2023]引入了一种新证明系统，关联工具VeriPB，至少比DRAT更强，并且还能处理某些对称性破坏技术。我们展示该系统模拟证明系统 $G_1$，后者允许有限的QBF推理，并形成ER在自然层次结构中下一层。该层次结构尚未被证明是严格的，但即便如此，这仍然是该系统相对于ER和DRAT可能严格更强的证据。反向地，我们展示，对单个对称性的对称性破坏可在ER内部处理。