# Orthologic for SAT Solving

arXiv: https://arxiv.org/abs/2605.16421 · HTML: https://mlsanity.com/paper/2605.16421/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 20 references that are in the map.
- First posted on arXiv 14 May 2026.

## Builds on (most cited first, 5 of 5)

- [System FR as Foundations for Stainless](https://mlsanity.com/paper/1904.03482/) (2019)
- [Focusing in Orthologic](https://mlsanity.com/paper/1612.01728/) (2016)
- [On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time](https://mlsanity.com/paper/2110.03315/) (2021)
- [Verified and Optimized Implementation of Orthologic Proof Search](https://mlsanity.com/paper/2501.09418/) (2025)
- [LISA -- A Modern Proof System](https://mlsanity.com/paper/2507.11167/) (2025)

## Abstract (arXiv)

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|)) worst-case complexity. We then introduce a family of synthetic SAT benchmarks based on the observation that, for any formula φ, the equivalence φ leftrightarrow NFOL(φ) 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.