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.

翻译：奇偶推理对冲突驱动子句学习（CDCL）SAT求解器具有挑战性。即使对于编码两个具有不同变量顺序的矛盾奇偶约束的简单公式，这一现象也已得到观察（Chew and Heule 2020）。我们通过证明当变量顺序随机选择时，这些公式以高概率需要指数规模的分解反驳，提供了其硬度的解析解释。我们通过证明这些已知为Tseitin公式的公式，其Tseitin图以高概率具有线性树宽来获得这一结果。由于这类Tseitin公式需要指数规模的分解证明，我们的结论随之成立。我们将这一论证推广到一类新公式，这类公式捕获涉及两个随机顺序的随机奇偶约束之和的基本奇偶推理形式。即使当和的变量顺序被有利地选择时，这些公式对分解而言仍然困难。相比之下，我们证明它们具有短的DRAT反驳。实验表明，CDCL SAT求解器在这两类公式上的运行时间随其树宽呈指数增长。