# The Computational Complexity of Satisfiability in State Space Models

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 18 references that are in the map.
- First posted on arXiv 25 Aug 2025.

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

- [Mamba: Linear-Time Sequence Modeling with Selective State Spaces](https://mlsanity.com/paper/2312.00752/) (2023)
- [Efficiently Modeling Long Sequences with Structured State Spaces](https://mlsanity.com/paper/2111.00396/) (2021)
- [Retentive Network: A Successor to Transformer for Large Language Models](https://mlsanity.com/paper/2307.08621/) (2023)
- [Gated Linear Attention Transformers with Hardware-Efficient Training](https://mlsanity.com/paper/2312.06635/) (2023)
- [Resurrecting Recurrent Neural Networks for Long Sequences](https://mlsanity.com/paper/2303.06349/) (2023)
- [Long Range Language Modeling via Gated State Spaces](https://mlsanity.com/paper/2206.13947/) (2022)
- [Griffin: Mixing Gated Linear Recurrences with Local Attention for Efficient Language Models](https://mlsanity.com/paper/2402.19427/) (2024)
- [The Illusion of State in State-Space Models](https://mlsanity.com/paper/2404.08819/) (2024)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [The Expressive Capacity of State Space Models: A Formal Language Perspective](https://mlsanity.com/paper/2405.17394/) (2024)
- [On the Expressiveness and Length Generalization of Selective State-Space Models on Regular Languages](https://mlsanity.com/paper/2412.19350/) (2024)
- [Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning](https://mlsanity.com/paper/2405.18548/) (2024)

## Built on by (most cited first, 1 of 1)

- [On the Expressiveness of State Space Models via Temporal Logics](https://mlsanity.com/paper/2601.19467/) (2026)

## Abstract (arXiv)

We analyse the complexity of the satisfiability problem ssmSAT for State Space Models (SSM), which asks whether an input sequence can lead the model to an accepting configuration. We find that ssmSAT is undecidable in general, reflecting the computational power of SSM. Motivated by practical settings, we identify two natural restrictions under which ssmSAT becomes decidable and establish corresponding complexity bounds. First, for SSM with bounded context length, ssmSAT is NP-complete when the input length is given in unary and in NEXPTIME (and PSPACE-hard) when the input length is given in binary. Second, for quantised SSM operating over fixed-width arithmetic, ssmSAT is PSPACE-complete resp. in EXPSPACE depending on the bit-width encoding. While these results hold for diagonal gated SSM we also establish complexity bounds for time-invariant SSM. Our results establish a first complexity landscape for formal reasoning in SSM and highlight fundamental limits and opportunities for the verification of SSM-based language models.