Orthologic for SAT Solving
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 worst-case complexity. We then introduce a family of synthetic SAT benchmarks based on the observation that, for any formula , the equivalence 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.
Cite
@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}
}