提出新算法，高效解决正交逻辑蕴含问题并加速特定难解SAT实例求解。
Orthologic for SAT Solving
- 基于正交逻辑归约设计新算法，省去昂贵预处理阶段。
- 在EPFL算术电路测试中，该算法可解Kissat超时的难例，且保持理论复杂度不变。
- 适用于需快速验证逻辑蕴含或提升硬核SAT求解效率的研究场景。
我们提出一种新的正交逻辑公式蕴含判定算法，避免了以往实现中的高成本预处理阶段，同时保持相同的$/mathcal{O}(n^2(1+|A|))$最坏时间复杂度。基于观察：对任意公式ϕ，等价式ϕ↔NF_{OL}(ϕ)是永真式，其Tseitin编码产生对当前主流SAT求解器极难的不可满足实例，但拥有简短的正交逻辑证明。将该算法应用于EPFL算术电路，其能高效求解这些实例，而Kissat在大量案例上超时。此外，我们证明以正交逻辑归约为预处理步骤，可显著改善某些难题的SAT求解时间。
原文摘要 · Abstract (English)
We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementations while retaining the same $\mathcal{O}(n^2(1+|A|))$ worst-case complexity. We then introduce a family of synthetic SAT benchmarks based on the observation that, for any formula $ϕ$, the equivalence $ϕ\leftrightarrow \mathrm{NF}_{\mathrm{OL}}(ϕ)$ is a tautology whose Tseitin encoding yields unsatisfiable instances that are hard for state-of-the-art SAT solvers yet have short orthologic proofs. Applied to EPFL arithmetic circuits, our algorithm solves these instances efficiently while Kissat times out on a significant fraction. Finally, we show that using orthologic normalization as a preprocessing step can improve SAT solving time on some hard problems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。