奇偶校验的随机重排序编码在归结法与CDCL下的难解性
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
AI总结：
本研究针对CDCL SAT求解器处理奇偶推理公式的难题，证明随机变量顺序的矛盾奇偶约束公式因Tseitin图线性树宽需指数级归结反驳，推广到新公式类仍难解但有短DRAT反驳，且实验验证运行时间随树宽指数增长。
摘要：
奇偶推理对冲突驱动子句学习（Conflict-Driven Clause Learning，CDCL）SAT求解器而言颇具挑战。即便对于编码了两个变量顺序不同的矛盾奇偶约束的简单公式，这一现象也已被观测到（Chew和Heule，2020）。我们通过证明当变量顺序随机选取时，这类公式以高概率需要指数级的归结反驳，为其难解性提供了分析层面的解释。我们通过证明这些已知属于Tseitin公式的公式，其Tseitin图以高概率具有线性树宽，得到了这一结果。由于这类Tseitin公式需要指数级的归结证明，我们的结论随之成立。我们将这一论证推广到一类新的公式，这类公式刻画了一种基本的奇偶推理形式，涉及两个随机顺序的随机奇偶约束之和。即便和的变量顺序被有利地选取，这些公式对归结法而言仍然难解。与之相对，我们证明它们存在短的DRAT反驳。我们通过实验表明，CDCL SAT求解器在这两类公式上的运行时间随其树宽呈指数增长。
英文摘要：
Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution proofs, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
