Orthologic for SAT Solving

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.