# Deconstructing Subset Construction -- Reducing While Determinizing

arXiv: https://arxiv.org/abs/2505.10319 · HTML: https://mlsanity.com/paper/2505.10319/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 58 references that are in the map.
- First posted on arXiv 15 May 2025.

## Builds on (most cited first, 7 of 7)

- [Fast and exact analysis for LRU caches](https://mlsanity.com/paper/1811.01670/) (2018)
- [Automatic Theorem Proving in Walnut](https://mlsanity.com/paper/1603.06017/) (2016)
- [Efficient reduction of nondeterministic automata with application to language inclusion testing](https://mlsanity.com/paper/1711.09946/) (2017)
- [Nested Antichains for WS1S](https://mlsanity.com/paper/1501.03849/) (2015)
- [The First-Order Theory of Binary Overlap-Free Words is Decidable](https://mlsanity.com/paper/2209.03266/) (2022)
- [Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)](https://mlsanity.com/paper/2403.18995/) (2024)
- [Data Structures for Finite Downsets of Natural Vectors: Theory and Practice](https://mlsanity.com/paper/2502.09189/) (2025)

## Abstract (arXiv)

We present a novel perspective on the NFA canonization problem, which introduces intermediate minimization steps to reduce the exploration space on-the-fly. Central to our approach are equivalence registries which track and unify language-equivalent states, and allow for additional optimizations such as convexity closures and simulation. Due to the generality of our approach, these concepts can be embedded in classic subset construction or Brzozowski's approach. We evaluate our approach on a set of synthetic and real-world examples from automatic sequences and observe that we are able to improve especially worst-case scenarios. We provide an open-source library implementing our approach.
