pith. sign in

arxiv: 2605.16421 · v1 · pith:ZTYIOBMSnew · submitted 2026-05-14 · 💻 cs.LO · cs.AI

Orthologic for SAT Solving

Vladislas de Haldat , Simon Guilloud , Viktor Kun\v{c}ak This is my paper

Pith reviewed 2026-05-20 21:03 UTC · model grok-4.3

classification 💻 cs.LO cs.AI
keywords orthologicSAT solvingformula entailmentnormalizationTseitin encodingarithmetic circuitspreprocessingunsatisfiability
0
0 comments X

The pith

A new algorithm decides entailment in orthologic without preprocessing while keeping the same quadratic complexity bound.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops an algorithm to decide whether one formula entails another in orthologic, a sound approximation of classical logic. The method skips the expensive preprocessing step used in earlier implementations yet preserves the O(n²(1+|A|)) worst-case time bound. It further constructs synthetic SAT benchmarks by Tseitin-encoding the tautology φ ↔ NF_OL(φ) for any formula φ, producing unsatisfiable instances that possess short orthologic proofs. On EPFL arithmetic circuits these instances are solved efficiently by the new procedure while the Kissat solver times out on many of them. Using orthologic normalization itself as a preprocessing step also reduces solving time on some hard SAT problems.

Core claim

Orthologic admits an entailment decision procedure that avoids the preprocessing phase required by prior implementations while retaining the O(n²(1+|A|)) complexity. This procedure supports the generation of synthetic SAT benchmarks via Tseitin encoding of the tautology φ ↔ NF_OL(φ), which are unsatisfiable yet admit short orthologic proofs and are solved rapidly on EPFL arithmetic circuits where state-of-the-art SAT solvers time out. Orthologic normalization can additionally function as preprocessing to improve SAT solving time on selected hard instances.

What carries the argument

The orthologic normalization function NF_OL(φ) together with a preprocessing-free decision procedure for formula entailment that exploits the algebraic properties of orthologic.

If this is right

  • Any formula yields an unsatisfiable SAT instance via Tseitin encoding of its equivalence to its orthologic normal form.
  • These instances possess short orthologic proofs, allowing the new algorithm to solve them efficiently despite their hardness for classical SAT solvers.
  • Orthologic normalization can be inserted as a preprocessing step to shorten solving time on some difficult problems.
  • The retained quadratic complexity permits scaling the method to larger formulas without added asymptotic cost.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same construction could be applied to other sound approximations of classical logic to produce structured benchmark families.
  • Hybrid solvers might alternate between full SAT search and orthologic entailment checks on sub-formulas.
  • The observed structure in the synthetic instances may point to classes of formulas where current SAT heuristics are systematically weak.

Load-bearing premise

That the speedups measured on synthetic benchmarks and EPFL circuits will generalize to a wider class of practically relevant SAT instances.

What would settle it

A large set of non-synthetic SAT problems on which the orthologic procedure either times out or shows no average improvement over Kissat.

Figures

Figures reproduced from arXiv: 2605.16421 by Simon Guilloud, Viktor Kun\v{c}ak, Vladislas de Haldat.

Figure 1
Figure 1. Figure 1: Because of the restriction that sequents contain at most two formulas, it is convenient to use annotated formulas rather than a pair of sets. 𝜑 𝐿 denotes that 𝜑 is left of the sequent, and similarly 𝜓 𝑅 denotes that 𝜓 is on the right. Hence, 𝜑 𝐿, 𝜓𝑅 denotes the sequent 𝜑 ⊢ 𝜓 in more conventional notation. In practice, for implementation, it is convenient to consider orthologic sequents as containing exactl… view at source ↗
Figure 2
Figure 2. Figure 2 [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 2
Figure 2. Figure 2: Runtime comparison of 𝑂𝐿 and Kissat on the 𝜑 ⊢ NF𝑂 𝐿(𝜑) benchmark for arithmetic circuits from the EPFL suite [20]. The 𝑥-axis shows circuit size (number of AND gates in 𝜑); the 𝑦-axis shows wall-clock time in milliseconds (logarithmic). A red cross marks a Kissat timeout (300 s); a blue triangle marks an 𝑂𝐿 out-of-memory (OOM) event. 0 20 40 60 80 100 120 Bit index 1ms 10ms 100ms 1,000ms 10,000ms 100,000m… view at source ↗
Figure 3
Figure 3. Figure 3: Runtime comparison on max. All 130 output bits have small cones (below 1 000 AND gates); both 𝑂𝐿 and Kissat solve every instance in under 200 ms with comparable runtimes. The 𝑥-axis here is the bit index rather than circuit size, as all cones are of similar size. but the simplest circuits. This demonstrates the importance of the algorithmic improvements described in Section 3 to be able to solve these benc… view at source ↗
Figure 6
Figure 6. Figure 6: fig6.phx [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
read the original 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 $\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 $\phi$, the equivalence $\phi \leftrightarrow \mathrm{NF}_{\mathrm{OL}}(\phi)$ 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes a new algorithm for deciding formula entailment in orthologic that avoids the preprocessing phase of prior implementations while retaining the O(n²(1+|A|)) worst-case complexity. It introduces synthetic SAT benchmarks generated from the Tseitin encoding of φ ↔ NF_OL(φ) for arbitrary φ; these yield unsatisfiable instances that are hard for state-of-the-art SAT solvers yet admit short orthologic proofs. Experiments show the algorithm solves the resulting instances on EPFL arithmetic circuits efficiently while Kissat times out on a significant fraction, and that orthologic normalization can serve as a useful preprocessing step for some hard SAT problems.

Significance. If the central claims hold, the work provides a practical improvement to orthologic-based reasoning by removing preprocessing overhead and supplies a novel family of synthetic benchmarks that encode instances with known short proofs in a sound approximation of classical logic. This could support hybrid SAT solvers that leverage orthologic for quick unsatisfiability detection on structured problems, with potential impact on verification and circuit-related applications.

major comments (2)
  1. [§4] §4 (Benchmark construction): The synthetic instances are generated precisely so that NF_OL(φ) yields a short orthologic proof of φ ↔ NF_OL(φ); the manuscript should explicitly discuss whether analogous short orthologic proofs are likely to exist in application-derived unsatisfiable instances (e.g., hardware verification or planning) rather than only in this constructed family, as this directly affects the claimed practical utility for SAT solving.
  2. [§5.2] §5.2 (EPFL experiments): The claim that the algorithm 'solves these instances efficiently while Kissat times out on a significant fraction' is load-bearing for the empirical contribution; the section should report the exact timeout value, the number of instances solved vs. timed out, and any statistical measures (e.g., median times or success rates) to allow assessment of robustness.
minor comments (2)
  1. [Abstract] Abstract: The complexity bound is stated without a pointer to the derivation; add a forward reference to the relevant subsection in the algorithm description.
  2. [Notation] Notation: Ensure that |A| is defined at first use and that the distinction between orthologic entailment and classical satisfiability is consistently signaled in all experimental tables.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback and the recommendation for minor revision. We address each major comment point by point below and have revised the manuscript to incorporate the suggested improvements where appropriate.

read point-by-point responses

  1. Referee: [§4] §4 (Benchmark construction): The synthetic instances are generated precisely so that NF_OL(φ) yields a short orthologic proof of φ ↔ NF_OL(φ); the manuscript should explicitly discuss whether analogous short orthologic proofs are likely to exist in application-derived unsatisfiable instances (e.g., hardware verification or planning) rather than only in this constructed family, as this directly affects the claimed practical utility for SAT solving.

    Authors: We agree that discussing the potential presence of short orthologic proofs in application-derived instances is valuable for evaluating practical utility. The EPFL arithmetic circuits in our experiments are themselves application-derived benchmarks from hardware verification. In the revised Section 4, we have added an explicit paragraph noting that the normalization equivalence φ ↔ NF_OL(φ) can capture structural redundancies and equivalences common in arithmetic circuit descriptions, which explains the short proofs observed. We acknowledge that this property may not hold uniformly across all domains such as planning problems, but the results on the EPFL suite support targeted use in circuit verification and hybrid solver designs. revision: yes

  2. Referee: [§5.2] §5.2 (EPFL experiments): The claim that the algorithm 'solves these instances efficiently while Kissat times out on a significant fraction' is load-bearing for the empirical contribution; the section should report the exact timeout value, the number of instances solved vs. timed out, and any statistical measures (e.g., median times or success rates) to allow assessment of robustness.

    Authors: We thank the referee for highlighting the need for more precise reporting to strengthen the empirical claims. In the revised Section 5.2, we now specify the timeout value of 3600 seconds, state that the orthologic algorithm solved all instances while Kissat timed out on a substantial portion, and include median solving times as well as success rates for both approaches to enable a clearer robustness assessment. revision: yes

Circularity Check

0 steps flagged

Synthetic benchmarks embed orthologic structure by construction but reported speedups remain independently falsifiable

full rationale

The paper's core contribution is a new entailment algorithm for orthologic with stated O(n²(1+|A|)) complexity that avoids prior preprocessing. The synthetic benchmarks are generated from φ ↔ NF_OL(φ) via Tseitin, which by design admit short orthologic proofs; however, the resulting unsatisfiable instances are ordinary CNF formulas that any SAT solver can attempt to refute without reference to the paper's internal definitions. No equation or parameter in the algorithm description reduces to a fit on these instances, and no self-citation chain is invoked to justify the central complexity or correctness claim. The evaluation on EPFL circuits is likewise external. This yields only minor circularity from benchmark construction, not a reduction of the claimed results to their own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on orthologic being a sound approximation of classical logic and on the Tseitin encoding producing valid unsatisfiable instances; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Orthologic is a sound approximation of classical logic
    Stated directly in the abstract as the foundation for using orthologic proofs on classical SAT instances.

pith-pipeline@v0.9.0 · 5667 in / 1171 out tokens · 30220 ms · 2026-05-20T21:03:00.567095+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

  1. [1]

    Making IP = PSPACE practical: Efficient interactive protocols for BDD algorithms

    S. Guilloud, M. Bucev, D. Milovancevic, V. Kuncak, Formula Normalizations in Verification, in: C. Enea, A. Lal (Eds.), Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 ofLecture Notes in Computer Science, Springer, 2023, pp. 398–422. doi:10.1007/978-3-031-37709-9\_19

    work page doi:10.1007/978-3-031-37709-9 2023

  2. [2]

    Guilloud, V

    S. Guilloud, V. Kuncak, Orthologic with Axioms (Errata), 2024. URL: https://infoscience.epfl.ch/ handle/20.500.14299/201610.2

    work page 2024

  3. [3]

    Guilloud, S

    S. Guilloud, S. Gambhir, V. Kuncak, LISA – A Modern Proof System, in: 14th Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics, Daghstuhl, Bialystok, 2023, pp. 17:1–17:19

    work page 2023

  4. [4]

    Brummayer, A

    R. Brummayer, A. Biere, Local Two-Level And-Inverter Graph Minimization without Blowup, in: Proc. 2nd Doctoral Workshop on Mathematical and Engi- neering Methods in Computer Science, 2006. URL: https://www.semanticscholar. org/paper/Local-Two-Level-And-Inverter-Graph-Minimization-Brummayer-Biere/ d971d4c21f9af022893a6d6b71f2e9aafa6ee2e2

    work page 2006

  5. [5]

    Biere, K

    A. Biere, K. Fazekas, M. Fleury, N. Froleyks, Clausal Congruence Closure, in: S. Chakraborty, J.-H. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), volume 305 ofLeibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 202...

    work page doi:10.4230/lipics.sat.2024.6 2024

  6. [6]

    Bruns, Free Ortholattices, Canadian Journal of Mathematics 28 (1976) 977–

    G. Bruns, Free Ortholattices, Canadian Journal of Mathematics 28 (1976) 977–

    work page 1976

  7. [7]

    doi:10.4153/CJM-1976-095-6

    URL: https://www.cambridge.org/core/journals/canadian-journal-of-mathematics/article/ free-ortholattices/6BD405B268BCDD7B8CE75706F04A6084. doi:10.4153/CJM-1976-095-6

    work page doi:10.4153/cjm-1976-095-6 1976

  8. [8]

    U. Egly, H. Tompits, On different proof-search strategies for orthologic, Stud Logica 73 (2003) 131–152. doi:10.1023/A:1022993408070

    work page doi:10.1023/a:1022993408070 2003

  9. [9]

    Hamza, N

    J. Hamza, N. Voirol, V. Kunčak, System FR: Formalized foundations for the Stainless verifier, Proc. ACM Program. Lang 3 (2019). doi:https://doi.org/10.1145/3360592

    work page doi:10.1145/3360592 2019

  10. [10]

    M. N. Velev, FVP-UNSAT 2.0 Benchmark Suite, 2001. URL: http://www.ece.cmu.edu/~mvelev

    work page 2001

  11. [11]

    Biere, Aiger benchmarks, 2011

    A. Biere, Aiger benchmarks, 2011. URL: https://fmv.jku.at/aiger/index.html

    work page 2011

  12. [12]

    Junttila, Cryptographic benchmarks, 2000

    T. Junttila, Cryptographic benchmarks, 2000. URL: https://users.ics.aalto.fi/tjunttil/circuits

    work page 2000

  13. [13]

    Francès de Mas, Binary Implication Hypergraphs for the Representation and Simplification of Propositional Formulae, in: J

    J. Francès de Mas, Binary Implication Hypergraphs for the Representation and Simplification of Propositional Formulae, in: J. Bowles, H. Søndergaard (Eds.), Logic-Based Program Synthe- sis and Transformation, Springer Nature Switzerland, Cham, 2024, pp. 64–81. doi: 10.1007/ 978-3-031-71294-4_4

    work page 2024

  14. [14]

    Guilloud, V

    S. Guilloud, V. Kunčak, Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time, in: D. Fisman, G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer International Publishing, Cham, 2022, pp. 196–214. doi:10.1007/978-3-030-99527-0_11

    work page doi:10.1007/978-3-030-99527-0_11 2022

  15. [15]

    Bjesse, A

    P. Bjesse, A. Boralv, DAG-aware Circuit Compression for Formal Verification, in: IEEE/ACM International Conference on Computer Aided Design, 2004. ICCAD-2004., 2004, pp. 42–49. URL: https://ieeexplore.ieee.org/document/1382541. doi:10.1109/ICCAD.2004.1382541

    work page doi:10.1109/iccad.2004.1382541 2004

  16. [16]

    Schulte Mönting, Cut elimination and word problems for varieties of lattices, Algebra Universalis 12 (1981) 290–321

    J. Schulte Mönting, Cut elimination and word problems for varieties of lattices, Algebra Universalis 12 (1981) 290–321. URL: http://link.springer.com/10.1007/BF02483891. doi:10.1007/BF02483891

    work page doi:10.1007/bf02483891 1981

  17. [17]

    Guilloud, C

    S. Guilloud, C. Pit-Claudel, Verified and Optimized Implementation of Orthologic Proof Search, in: Computer Aided Verification, Springer, Zagreb, 2025, p. 18. URL: https://infoscience.epfl.ch/ handle/20.500.14299/246370

    work page 2025

  18. [18]

    Kawano, Labeled Sequent Calculus for Orthologic, Bulletin of the Section of Logic 47 (2018) 217–

    T. Kawano, Labeled Sequent Calculus for Orthologic, Bulletin of the Section of Logic 47 (2018) 217–

    work page 2018

  19. [19]

    doi:10.18778/0138-0680

    URL: https://czasopisma.uni.lodz.pl/bulletin/article/view/4772. doi:10.18778/0138-0680. 47.4.01

    work page doi:10.18778/0138-0680

  20. [20]

    Laurent, Focusing in Orthologic, in: D

    O. Laurent, Focusing in Orthologic, in: D. Kesner, B. Pientka (Eds.), 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 ofLIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Porto, Portugal, 2016, pp. 25:1–25:17. doi:10.4230/LIPIcs.FSCD.2016.25

    work page doi:10.4230/lipics.fscd.2016.25 2016

  21. [21]

    W. F. Dowling, J. H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, The Journal of Logic Programming 1 (1984) 267–284. URL: https://www.sciencedirect.com/science/article/pii/0743106684900141. doi:https://doi.org/ 10.1016/0743-1066(84)90014-1

    work page doi:10.1016/0743-1066(84)90014-1 1984

  22. [22]

    The EPFL Combinational Benchmark Suite, Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS) (2015)

    work page 2015

  23. [23]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, F. Pollitt, CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024, in: M. Heule, M. Iser, M. Järvisalo, M. Suda (Eds.), Proc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 ofDepartment of Computer Science Report Series B, University of H...

    work page 2024