# Solvability of orbit-finite systems of linear equations

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 38 references that are in the map.
- First posted on arXiv 22 Jan 2022.

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

- [Automata theory in nominal sets](https://mlsanity.com/paper/1402.0897/) (2014)
- [The Reachability Problem for Petri Nets is Not Primitive Recursive](https://mlsanity.com/paper/2104.12695/) (2021)
- [Demystifying Reachability in Vector Addition Systems](https://mlsanity.com/paper/1503.00745/) (2015)
- [Reachability in Vector Addition Systems is Ackermann-complete](https://mlsanity.com/paper/2104.13866/) (2021)
- [Linear Equations with Ordered Data](https://mlsanity.com/paper/1802.06660/) (2018)
- [Improved Ackermannian lower bound for the Petri nets reachability problem](https://mlsanity.com/paper/2105.08551/) (2021)
- [Reachability analysis of first-order definable pushdown systems](https://mlsanity.com/paper/1504.02651/) (2015)
- [Linear Combinations of Unordered Data Vectors](https://mlsanity.com/paper/1610.01470/) (2016)
- [Parikh's theorem for infinite alphabets](https://mlsanity.com/paper/2104.12018/) (2021)

## Abstract (arXiv)

We study orbit-finite systems of linear equations, in the setting of sets with atoms. Our principal contribution is a decision procedure for solvability of such systems. The procedure works for every field (and even commutative ring) under mild effectiveness assumptions, and reduces a given orbit-finite system to a number of finite ones: exponentially many in general, but polynomially many when atom dimension of input systems is fixed. Towards obtaining the procedure we push further the theory of vector spaces generated by orbit-finite sets, and show that each such vector space admits an orbit-finite basis. This fundamental property is a key tool in our development, but should be also of wider interest.