# Boolean Abstractions for Realizability Modulo Theories (Extended version)

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Oct 2023.

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

- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [Realizable Continuous-Space Shields for Safe Reinforcement Learning](https://mlsanity.com/paper/2410.02038/) (2024)
- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)
- [SemML 2.0: Synthesizing Controllers for LTL](https://mlsanity.com/paper/2604.24102/) (2026)
- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)
- [Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2602.06227/) (2026)
- [Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications](https://mlsanity.com/paper/2603.06710/) (2026)
- [Is Your Agent Playing Dead? Deployed LLM Agents Exhibit Constraint-Evasive Fabrication and Thanatosis](https://mlsanity.com/paper/2606.14831/) (2026)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)

## Abstract (arXiv)

In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables imposed by the literals. The resulting specification can be passed to existing Boolean off-the-shelf realizability tools, and is realizable if and only if the original specification is realizable. The first contribution is a brute-force version of our method, which requires a number of SMT queries that is doubly exponential in the number of input literals. Then, we present a faster method that exploits a nested encoding of the search for the extra requirement and uses SAT solving for faster traversing the search space and uses SMT queries internally. Another contribution is a prototype in Z3-Python. Finally, we report an empirical evaluation using specifications inspired in real industrial cases. To the best of our knowledge, this is the first method that succeeds in non-Boolean LTL realizability.