Document Open Access Logo

Efficient Identification of Isomorphic SAT Instances (Tool Paper)

Authors Ashlin Iser , Frederick Gehm

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.35.pdf
  • Filesize: 1.34 MB
  • 8 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Design and analysis of algorithms
  • Information systems → Information integration
Keywords
  • Isomorphism
  • Benchmarking
  • Boolean Satisfiability

Metrics

Abstract

Many SAT benchmark datasets contain structurally identical instances arising from repeated shuffling, generators producing identical formulas under different seeds, or duplicate encodings from different tools. We present an efficient, open-source, isomorphism-invariant hashing algorithm for SAT instances, based on Weisfeiler-Leman (WL) label refinement. Each instance is represented as a bipartite clause-literal graph, and iterative label refinement computes a canonical signature, with instances having identical signatures treated as isomorphic. When integrated into our benchmark toolset Global Benchmark Database (GBD), the method substantially reduces false positives from naive degree-sequence hashing with minimal overhead.

Cite As Get BibTex

Ashlin Iser and Frederick Gehm. Efficient Identification of Isomorphic SAT Instances (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 35:1-35:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.35

Author Details

Ashlin Iser
  • Karlsruhe Institute of Technology, Germany
Frederick Gehm
  • Karlsruhe Institute of Technology, Germany

Acknowledgements

We thank Timon Passlick for his BA thesis on early explorations of fast isomorphism detection.

Supplementary Materials

References

  1. Markus Anders. Efficient Algorithms for Symmetry Detection. PhD thesis, Technische Universität Darmstadt, 2024. URL: https://doi.org/10.26083/tuprints-00028257.
  2. László Babai. Graph Isomorphism in Quasipolynomial Time [extended abstract]. In ACM Symposium on Theory of Computing, STOC, 2016. URL: https://doi.org/10.1145/2897518.2897542.
  3. László Babai and Ludik Kucera. Canonical Labelling of Graphs in Linear Average Time. In Symposium on Foundations of Computer Science, SFCS, 1979. URL: https://doi.org/10.1109/SFCS.1979.8.
  4. Armin Biere and Marijn Heule. The Effect of Scrambling CNFs. In Pragmatics of SAT, 2018. Google Scholar
  5. Jin-yi Cai, Martin Fürer, and Neil Immerman. An Optimal Lower Bound on the Number of Variables for Graph Identification. Combinatorica, 1992. URL: https://doi.org/10.1007/BF01305232.
  6. Yifan Feng, Jiashu Han, Shihui Ying, and Yue Gao. Hypergraph Isomorphism Computation. IEEE Trans. Pattern Anal. Mach. Intell., 2024. URL: https://doi.org/10.1109/TPAMI.2024.3353199.
  7. Ashlin Iser. Benchmark Compilation for SAT Competition 2023. In Proceedings of SAT Competition, 2023. URL: http://hdl.handle.net/10138/563824.
  8. Ashlin Iser and Frederick Gehm. Global Benchmark Database. Software, (visited on 2026-07-03). URL: https://github.com/udopia/gbdc
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26969
  9. Ashlin Iser and Frederick Gehm. IsoHash2 Implementation in GBDC. https://github.com/Udopia/gbdc/blob/master/src/identify/ISOHash2.h, 2026. Accessed: 2026-03-09.
  10. Ashlin Iser and Christoph Jabs. Global Benchmark Database. In Intl. Conference on Theory and Applications of Satisfiability Testing, SAT, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.18.
  11. Ashlin Iser and Christoph Jabs. Global Benchmark Database (extension module), 2024. URL: https://doi.org/10.4230/ARTIFACTS.22457.
  12. Tommi Junttila and Petteri Kaski. Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs. In Workshop on Algorithm Engineering and Experiments, ALENEX, 2007. Google Scholar
  13. Brendan D. McKay and Adolfo Piperno. Practical Graph Isomorphism, II. J. Symb. Comput., 2014. URL: https://doi.org/10.1016/J.JSC.2013.09.003.
  14. Ilya Otpuschennikov, Alexander Semenov, Victor Kondratiev, Daniil Chivilikhin, and Stepan Kochemazov. Benchmarks Encoding Logical Equivalence Checking for Sorting Algorithms. In Proceedings of SAT Competition, 2022. URL: http://hdl.handle.net/10138/359079.
  15. Nino Shervashidze, Pascal Schweitzer, Erik Jan van Leeuwen, Kurt Mehlhorn, and Karsten M. Borgwardt. Weisfeiler-Lehman Graph Kernels. Journal of Machine Learning Research, 2011. URL: http://jmlr.org/papers/v12/shervashidze11a.html.
  16. Ivor T. A. Spence. sgen1: A Generator of Small but Difficult Satisfiability Benchmarks. ACM J. Exp. Algorithmics, 2010. URL: https://doi.org/10.1145/1671970.1671972.
  17. Guy L. Steele, Doug Lea, and Christine H. Flood. Fast Splittable Pseudorandom Number Generators. In ACM Intl. Conf. on Object Oriented Programming Systems Languages and Applications, OOPSLA, 2014. URL: https://doi.org/10.1145/2660193.2660195.
  18. Boris Weisfeiler and Andrei Leman. Reduction of a Graph to a Canonical Form and an Algebra Arising During this Reduction. Nauchno-Technicheskaya Informatsiya, 1968. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact