Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Detecting Isohedral Polyforms with a SAT Solver

Craig S. Kaplan

TL;DR

Kaplan presents a SAT-based framework to decide whether a polyform $T$ tiles the plane isohedrally by encoding surroundability constraints and the extendable-surround Local criterion into Boolean formulas. The method expresses the isohedral question for $T$ in terms of a surround $S$ consisting of copies $T_i = g_i(T)$ for $i=1,\dots,n$ and enforces extendability and mutual consistency across layers, enabling integration with his prior SAT-based Heesch-number computation. The augmented SAT formulation yields a solver-based tool that reproduces known isohedral counts and generalizes across polyform grids without hand-tuned isohedral-type logic, although it remains slower than specialized algorithms. The work also outlines practical limitations, notably in handling $k$-anisohedral cases (for $k \ge 2$) and aperiodic monotiles, suggesting directions toward discrete-optimization enhancements. Overall, it provides a flexible, software-friendly route to certify isohedral tilings within a unified SAT framework.

Abstract

I show how to express the question of whether a polyform tiles the plane isohedrally as a Boolean formula that can be tested using a SAT solver. This approach is adaptable to a wide range of polyforms, requires no special-case code for different isohedral tiling types, and integrates seamlessly with existing software for computing Heesch numbers of polyforms.

Detecting Isohedral Polyforms with a SAT Solver

TL;DR

Kaplan presents a SAT-based framework to decide whether a polyform tiles the plane isohedrally by encoding surroundability constraints and the extendable-surround Local criterion into Boolean formulas. The method expresses the isohedral question for in terms of a surround consisting of copies for and enforces extendability and mutual consistency across layers, enabling integration with his prior SAT-based Heesch-number computation. The augmented SAT formulation yields a solver-based tool that reproduces known isohedral counts and generalizes across polyform grids without hand-tuned isohedral-type logic, although it remains slower than specialized algorithms. The work also outlines practical limitations, notably in handling -anisohedral cases (for ) and aperiodic monotiles, suggesting directions toward discrete-optimization enhancements. Overall, it provides a flexible, software-friendly route to certify isohedral tilings within a unified SAT framework.

Abstract

I show how to express the question of whether a polyform tiles the plane isohedrally as a Boolean formula that can be tested using a SAT solver. This approach is adaptable to a wide range of polyforms, requires no special-case code for different isohedral tiling types, and integrates seamlessly with existing software for computing Heesch numbers of polyforms.

Paper Structure

This paper contains 4 sections, 1 theorem.

Table of Contents

  1. Introduction
  2. Identifying prototiles based on surrounds
  3. SAT formulation
  4. Discussion

Key Result

Proposition 1

A shape $T$ admits an isohedral tiling if and only if $T$ has a surround $\mathcal{S}=\{T_1,\ldots,T_n\}$ in which every $T_i$ is extendable (in which case every tile in the tiling is surrounded by a congruent copy of $\mathcal{S}$).

Theorems & Definitions (1)

  • Proposition 1