A SAT Encoding to Compute Aperiodic Tiling Rhythmic Canons

TL;DR

This paper introduces a SAT encoding approach to find all aperiodic tiling complements of rhythms in mathematical music theory, enabling solutions for larger periods than previous algorithms.

Contribution

It presents a novel SAT encoding and ILP formulation that efficiently enumerates aperiodic tiling complements, extending the solvable period range in musical tiling problems.

Findings

Successfully enumerated all aperiodic tiling complements for Vuza rhythms at periods 180, 420, and 900.

Extended the computational limits of solving aperiodic tiling problems beyond previous algorithms.

Validated the SAT encoding with multiple periods and rhythms, demonstrating its effectiveness.

Abstract

In Mathematical Music theory, the Aperiodic Tiling Complements Problem consists in finding all the possible aperiodic complements of a given rhythm $A$. The complexity of this problem depends on the size of the period $n$ of the canon and on the cardinality of the given rhythm $A$. The current state-of-the-art algorithms can solve instances with $n$ smaller than $180$. In this paper we propose an ILP formulation and a SAT Encoding to solve this mathemusical problem, and we use the Maplesat solver to enumerate all the aperiodic complements. We validate our SAT Encoding using several different periods and rhythms and we compute for the first time the complete list of aperiodic tiling complements of standard Vuza rhythms for canons of period $n=\{180,420,900\}$.