结合$k$ - CNF和XOR相变
Combining the $k$-CNF and XOR Phase-Transitions
摘要：
现代SAT求解器在随机$k$ -CNF公式上的运行时性能与随机$k$ -CNF公式的可满足性中经验上看到的“相变”现象密切相关。最近通用的基于散列的采样和计数方法主要依赖于SAT求解器在表示为$k$ -CNF和XOR约束的结合的公式上的运行时性能（称为$k$ -CNF-XOR公式），但是随机$k$ -CNF-XOR公式的行为在先前的工作中未被探索。本文首次研究了随机$k$ -CNF-XOR公式的可满足性。我们展示了一个令人惊讶的相变的经验证据，遵循$k$ -CNF和XOR约束之间的线性权衡。进一步证明了对于$k = 2$和（当$k$-CNF约束的数目较少时）对于$k > 2$，$k$-CNF-XOR公式存在相变.
英文摘要：
The runtime performance of modern SAT solvers on random $k$-CNF formulas is deeply connected with the 'phase-transition' phenomenon seen empirically in the satisfiability of random $k$-CNF formulas. Recent universal hashing-based approaches to sampling and counting crucially depend on the runtime performance of SAT solvers on formulas expressed as the conjunction of both $k$-CNF and XOR constraints (known as $k$-CNF-XOR formulas), but the behavior of random $k$-CNF-XOR formulas is unexplored in prior work. In this paper, we present the first study of the satisfiability of random $k$-CNF-XOR formulas. We show empirical evidence of a surprising phase-transition that follows a linear trade-off between $k$-CNF and XOR constraints. Furthermore, we prove that a phase-transition for $k$-CNF-XOR formulas exists for $k = 2$ and (when the number of $k$-CNF constraints is small) for $k > 2$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
