Decidability of periodic 2-SAT ($HN_2$) on finitely generated word-hyperbolic groups and effective bounds on periodicity of solutions

Freedman (STOC 1998) generalized Boolean $k$-SAT to formulae indexed by a finitely generated group $G$: writing $N_k$ for the class of formulae that are conjunctions of $k$-clauses ($k$-CNF), an $H$-equivariant formula in $HN_k$ is the conjunction of all translates, by a finite-index subgroup $H$, of finitely many $k$-clauses over $G$-indexed literals, and satisfiability asks for an arbitrary — not necessarily periodic — truth assignment on $G$. He proved $HN_2$ decidable but $HN_3$ undecidable for $G=\mathbb{Z}\oplus\mathbb{Z}$, and that satisfiable $HN_2$ instances admit periodic solutions on $\mathbb{Z}^2$ and on finitely generated nilpotent groups. The open core addressed by this task is twofold: the conjecture, recorded in Freedman's STOC 1998 paper, that $HN_2$ is decidable for finitely generated word-hyperbolic groups, and explicit computable bounds on the periodicity index of satisfying assignments, which the source leaves unquantified.

Background

Classical Boolean satisfiability exhibits a sharp boundary at clause size two: satisfiability of conjunctions of 3-literal disjunctions (3-SAT) is NP-complete, while 2-SAT is solvable in polynomial time by computing reachability in the implication graph — the directed graph whose vertices are literals and whose edges record the implications forced by each 2-clause (a clause $x\vee y$ implies $\bar{x}\Rightarrow y$ and $\bar{y}\Rightarrow x$); a 2-CNF formula is satisfiable iff no variable $x$ has directed paths both from $x$ to its negation $\bar{x}$ and back.

Freedman (STOC 1998) introduced a group-indexed, infinitary generalization of this boundary. Fix an infinite, finitely generated group $G$ (a group generated by some finite set of elements) and a subgroup $H\subset G$ of finite index (i.e., $G$ is the union of finitely many cosets of $H$; the word metric on $G$ with respect to a finite generating set measures distance as the length of the shortest representing word). The source writes $N_k$ for the class of finite formulae that are conjunctions of $k$-clauses ($k$-CNF), and $HN_k$ for its $H$-equivariant, group-indexed analogue: a formula $F\in HN_k$ is a conjunction of $k$-clauses over literals indexed by elements of $G$, the clause family being closed under right multiplication by every $h\in H$; equivalently, $F$ is specified by finitely many clause orbits under the action of $H$. For $G=\mathbb{Z}\oplus\mathbb{Z}$ and $H=p\mathbb{Z}\oplus p\mathbb{Z}$ these are exactly the doubly periodic Boolean formulae, so the input is finite even though the formula itself is infinite. Satisfiability asks for a truth assignment $\alpha:G\to\{0,1\}$ satisfying every clause — crucially, $\alpha$ is not required to be periodic, so decidability does not follow from the finite quotient.

Freedman proved: (a) for $G=\mathbb{Z}$, satisfiable formulae always admit periodic satisfying assignments with an explicit period bound in the formula diameter and period, but the minimal solution period can exceed the formula period by an arbitrary factor, so naive bounds fail; (b) for $G=\mathbb{Z}\oplus\mathbb{Z}$, $HN_2$ is decidable — the implication-graph argument lifts to the infinite periodic setting once the local consistency conditions on the finite quotient are augmented by a homological integer-linear condition expressing that concatenations of implication arrows close up in $G$, checked by integer linear programming — while $HN_3$ is undecidable (in fact, for suitable instances, undecidable within the standard ZFC axioms of set theory) by encoding the classical undecidable plane-tiling (domino) problem — deciding whether a finite set of square tile types with matching edge-color rules can cover the plane — so the finite 2-versus-3 boundary survives infinitization; (c) every satisfiable $HN_2$ formula on $\mathbb{Z}\oplus\mathbb{Z}$, and more generally on any finitely generated nilpotent group (a group whose lower central series, the descending chain of iterated commutator subgroups, reaches the trivial subgroup after finitely many steps), admits a satisfying assignment that is periodic under some finite-index subgroup $H'\subset H$; (d) as a byproduct, 3-colorability of doubly periodic planar graphs is undecidable.

The $\mathbb{Z}^2$ and nilpotent arguments are, however, essentially commutative: compositions of implication arrows are projected onto complementary rank-one subgroups, and the closing-up condition becomes an abelian integer-linear system. Beyond the nilpotent (polynomial-growth) world, the natural large class is the word-hyperbolic groups: finitely generated groups whose geodesic triangles are uniformly $\delta$-thin in the word metric (equivalently, groups acting properly and cocompactly by isometries on negatively curved spaces); this class contains free groups, surface groups, and in a precise sense most groups of exponential growth. For these groups no analogue of the homological integer-linear condition is known, and the source leaves two things open: the conjecture that $HN_2$ is decidable for finitely generated word-hyperbolic groups, and an explicitly quantified version of the source's remark that integer-linear programming could in principle estimate an upper bound for the periodicity index in terms of the formula parameters.

Neighboring frameworks: the same $\mathbb{Z}^d$-indexed questions were studied from the 1980s under the names periodically specified problems and periodic graphs (graphs repeated by translation along a lattice), for which reachability and shortest paths are polynomial-time decidable (Höfting–Wanke); Chen recast Freedman's model as the periodic constraint satisfaction problem, and periodic 2-SAT over $\mathbb{Z}^d$ is solvable in polynomial time (Chen 2003/2005; MIT–ULB CompGeom Group 2025, via reduction to polynomial-time periodic reachability); and recent work on decision problems on finitely generated groups — notably the domino problem, conjectured to be decidable exactly on virtually free groups (groups with a free subgroup of finite index) — has revived the group-indexed viewpoint, including a modified group-valued k-SAT (Bitar). None of these lines treats periodic 2-SAT over non-abelian period groups.

Problem Statement

Let $G$ be an infinite finitely generated group and $H\subset G$ a subgroup of finite index. Let $HN_2(G,H)$ denote the class of Boolean formulae that are conjunctions of 2-clauses over $G$-indexed literals, the clause family being the union of the $H$-orbits (under right multiplication on literal indices) of a finite set of clauses. The decision problem for $HN_2(G,H)$ takes as input the finite clause-orbit description of a formula $F$ (finitely many representative clauses, with literal positions given by words over a fixed finite generating set of $G$, together with the coset structure of $H$ in $G$) and asks whether $F$ admits a satisfying truth assignment $\alpha:G\to\{0,1\}$, periodic or not; here $G$ and $H$ are fixed parameters of the problem and the instance is the finite description of $F$.

(1) Prove or refute the conjecture recorded in Freedman's STOC 1998 paper: for every finitely generated word-hyperbolic group $G$ — with $G$ effectively presented (e.g., by a finite presentation, together with whatever hyperbolicity data the procedure requires) — and every subgroup $H\subset G$ of finite index given by explicit finite data (e.g., a coset table, a finite table of the action of the generators of $G$ on the cosets of $H$), the decision problem for $HN_2(G,H)$ is decidable.

(2) Effective periodicity bounds: for $G=\mathbb{Z}\oplus\mathbb{Z}$, and more generally for the finitely generated nilpotent groups for which the existence of periodic satisfying assignments is known (with $G=\mathbb{Z}\oplus\mathbb{Z}$ as the base case and the whole nilpotent class as the full target), derive an explicit computable function $f$ of the instance parameters — the period index $[G:H]$, the clause diameter $d$ (the maximal word-metric distance between literals of a clause), and the number $m$ of clause orbits — such that every satisfiable $F\in HN_2(G,H)$ admits an $H'$-periodic satisfying assignment with $[H:H']\le f([G:H],d,m)$; or, in the converse direction, determine how fast the minimal such index must be allowed to grow by exhibiting an explicit infinite family of satisfiable instances whose certified minimal periodic-satisfaction indices grow without bound in those parameters.

These two parts form one objective: extending the decidability theory of periodic 2-SAT beyond the abelian/nilpotent groups where it currently rests, and making it effective. Part (2) is both a standalone refinement of the solved cases and the quantitative ingredient that any resolution of part (1) based on searching periodic assignments would require; already for $G=\mathbb{Z}$ the minimal solution period is an unbounded multiple of the formula period, so no trivial bound exists.

References

1. Michael H. Freedman, K-sat on groups and undecidability, Proceedings of the thirtieth annual ACM symposium on Theory of computing (STOC '98), ACM Press, 1998, pp. 572–576. DOI: 10.1145/276698.276871, https://doi.org/10.1145/276698.276871.
2. Michael H. Freedman, Limit, logic, and computation, Proceedings of the National Academy of Sciences USA 95(1):95–97, 1998. DOI: 10.1073/pnas.95.1.95, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC18137/.
3. Hubie Chen, Periodic Constraint Satisfaction Problems: Polynomial-Time Algorithms, Principles and Practice of Constraint Programming (CP 2003), Springer LNCS, 2003, pp. 199–213. DOI: 10.1007/978-3-540-45193-8_14, https://doi.org/10.1007/978-3-540-45193-8_14.
4. Hubie Chen, Periodic Constraint Satisfaction Problems: Tractable Subclasses, Constraints 10(2):97–113, 2005. DOI: 10.1007/s10601-005-0551-z, https://doi.org/10.1007/s10601-005-0551-z.
5. Stefan S. Dantchev, Frank D. Valencia, On the computational limits of infinite satisfaction, Proceedings of the 2005 ACM Symposium on Applied Computing (SAC 2005), ACM, 2005, pp. 393–397. DOI: 10.1145/1066677.1066768, https://doi.org/10.1145/1066677.1066768.
6. Bartek Klin, Eryk Kopczyński, Joanna Ochremiak, Szymon Toruńczyk, Locally Finite Constraint Satisfaction Problems, 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), 2015, pp. 475–486. DOI: 10.1109/LICS.2015.51, https://doi.org/10.1109/LICS.2015.51.
7. Nicolás Bitar, Contributions to the Domino Problem: Seeding, Recurrence and Satisfiability, Symposium on Theoretical Aspects of Computer Science (STACS 2024), LIPIcs, 2024, Art. 17, pp. 17:1–17:18. DOI: 10.4230/LIPIcs.STACS.2024.17, https://doi.org/10.4230/LIPIcs.STACS.2024.17; preprint arXiv:2312.08911, https://arxiv.org/abs/2312.08911.
8. MIT–ULB CompGeom Group (Zachary Abel, Hugo Akitaya, Lily Chung, Erik D. Demaine, Jenny Diomidova, Della Hendrickson, Stefan Langerman, Jayson Lynch), Undecidability of Tiling with a Tromino, arXiv:2509.07906, 2025. DOI: 10.48550/arXiv.2509.07906, https://arxiv.org/abs/2509.07906.
9. Antoine Cuvelier, Rémi Morvan, A Dichotomy Theorem for Automatic Structures, arXiv:2602.18238, 2026. DOI: 10.48550/arXiv.2602.18238, https://arxiv.org/abs/2602.18238.
10. Franz Höfting, Egon Wanke, Minimum Cost Paths in Periodic Graphs, SIAM Journal on Computing 24(5):1051–1067, 1995. DOI: 10.1137/s0097539792234378, https://doi.org/10.1137/s0097539792234378.
11. Franz Höfting, Egon Wanke, Polynomial-Time Analysis of Toroidal Periodic Graphs, Journal of Algorithms 34(1):14–39, 2000. DOI: 10.1006/jagm.1999.1046, https://doi.org/10.1006/jagm.1999.1046.
12. M. V. Marathe, H. B. Hunt III, R. E. Stearns, D. J. Rosenkrantz, Theory of periodically specified problems: Complexity and approximability, Los Alamos National Laboratory / University at Albany–SUNY technical report, 1997. DOI: 10.2172/587665, https://www.osti.gov/biblio/587665.
13. Madhav V. Marathe, Towards a Predictive Computational Complexity Theory, Automata, Languages and Programming (ICALP), Springer LNCS, 2002, pp. 22–31. DOI: 10.1007/3-540-45465-9_2, https://doi.org/10.1007/3-540-45465-9_2.
14. James Conant, Oliver Thistlethwaite, Boolean formulae, hypergraphs and combinatorial topology, Topology and its Applications 157(16):2449–2461, 2010. DOI: 10.1016/j.topol.2010.08.016, https://doi.org/10.1016/j.topol.2010.08.016; preprint arXiv:0808.0739, https://arxiv.org/abs/0808.0739.