Orthologic for SAT Solving
For SAT solving researchers, this work offers a new preprocessing technique that can speed up solving on certain hard instances, though the improvements are demonstrated on synthetic benchmarks and a limited set of problems.
The paper presents a new algorithm for orthologic entailment that avoids costly preprocessing while maintaining O(n^2(1+|A|)) complexity, and shows it efficiently solves synthetic SAT benchmarks that are hard for state-of-the-art solvers like Kissat, while also improving SAT solving time on some hard problems.
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.