Orthologic for SAT Solving

TL;DR

This paper introduces a new orthologic-based algorithm for SAT solving that improves efficiency and preprocessing, and demonstrates its effectiveness on synthetic benchmarks and real problems.

Contribution

The authors develop a novel orthologic algorithm that avoids costly preprocessing and enhances SAT solving performance on specific benchmarks and real-world instances.

Findings

The new algorithm matches the same worst-case complexity as prior methods.

It efficiently solves synthetic SAT instances that are hard for traditional solvers.

Orthologic normalization as preprocessing can improve SAT solving times on some problems.

Abstract

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 $\phi$, the equivalence $\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.