Orthologic for SAT Solving
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917502254055424 |
|---|---|
| author | de Haldat, Vladislas Guilloud, Simon Kunčak, Viktor |
| author_facet | de Haldat, Vladislas Guilloud, Simon Kunčak, Viktor |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_16421 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Orthologic for SAT Solving de Haldat, Vladislas Guilloud, Simon Kunčak, Viktor Logic in Computer Science Artificial Intelligence 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. |
| title | Orthologic for SAT Solving |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2605.16421 |