# Modulo Counting on Words and Trees

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Oct 2017.

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

- [A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers](https://mlsanity.com/paper/2605.03391/) (2026)

## Abstract (arXiv)

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.