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.

翻译：我们提出了一种新的算法，用于判定正交逻辑（经典逻辑的可靠近似）中的公式蕴含关系。该算法避免了以往实现中代价高昂的预处理阶段，同时保留了相同的$\mathcal{O}(n^2(1+|A|))$最坏情况复杂度。随后，基于以下观察，我们引入了一系列合成SAT基准测试：对于任意公式$φ$，等价式$φ\leftrightarrow \mathrm{NF}_{\mathrm{OL}}(φ)$是重言式，其Tseitin编码会产生对最先进的SAT求解器而言困难、但具有短正交逻辑证明的不可满足实例。应用于EPFL算术电路时，我们的算法高效地解决了这些实例，而Kissat在相当一部分实例上超时。最后，我们证明，将正交逻辑归一化作为预处理步骤，可以改善某些困难问题的SAT求解时间。