中文

Orthologic for SAT Solving

计算机科学中的逻辑 2026-05-19 v1 人工智能

摘要

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 O(n2(1+A))\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 ϕ\phi, the equivalence ϕNFOL(ϕ)\phi \leftrightarrow \mathrm{NF}_{\mathrm{OL}}(\phi) 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.

关键词

引用

@article{arxiv.2605.16421,
  title  = {Orthologic for SAT Solving},
  author = {Vladislas de Haldat and Simon Guilloud and Viktor Kunčak},
  journal= {arXiv preprint arXiv:2605.16421},
  year   = {2026}
}