针对 Resolution 与 CDCL 的奇偶校验随机重排编码的难度
计算复杂性
2024-02-02 v1
摘要
奇偶校验推理对于冲突驱动子句学习(CDCL)SAT 求解器而言是一项挑战。即使对于编码具有不同变量顺序的两个矛盾奇偶校验约束的简单公式,这也已被观察到(Chew 和 Heule 2020)。我们通过证明当变量顺序随机选择时,它们以高概率需要指数级的 Resolution 反证,为其难度提供了解析解释。我们通过证明这些公式(已知为 Tseitin 公式)以高概率具有线性树宽的 Tseitin 图来获得这一结果。由于此类 Tseitin 公式需要指数级的 Resolution 证明,因此我们的结果成立。我们将此论证推广到一类新公式,这类公式捕获了涉及具有随机顺序的两个随机奇偶校验约束之和的奇偶校验推理的基本形式。即使为和选择有利的变量顺序,这些公式对 Resolution 而言仍然困难。相比之下,我们证明它们具有较短的 DRAT 反证。我们通过实验表明,CDCL SAT 求解器在这两类公式上的运行时间随其树宽呈指数增长。
引用
@article{arxiv.2402.00542,
title = {Hardness of Random Reordered Encodings of Parity for Resolution and CDCL},
author = {Leroy Chew and Alexis de Colnet and Friedrich Slivovsky and Stefan Szeider},
journal= {arXiv preprint arXiv:2402.00542},
year = {2024}
}