Constraints JournalHappy Monday everyone!
Here's something to brighten up the start of your week: a paper about solving mathemusical problems with ILP and SAT, from our latest issue:
Computing aperiodic tiling rhythmic canons via SAT models
https://link.springer.com/article/10.1007/s10601-024-09375-6
To make this Monday extra sweet: the authors use MapleSAT!
#Mathematics
#Music
#ConstraintProgramming
#AI
#Rhythm
#AcademicMastodon
#BooleanSatisfiability
#AperiodicTiling
#MapleSAT
#ILP
#CombinatorialAlgorithms
#ArtificialIntelligence
Computing aperiodic tiling rhythmic canons via SAT models - Constraints
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 $$\varvec{180}$$ 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 then enhance the SAT model in two different ways. First, we enforce the SAT model with a set of clauses that retrieves the solutions up to translation. Second, we propose a decomposition of the solution space that allows to parallelize the resolution of the problem. We validate our different models 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 with period $$\varvec{n} = \varvec{\left\{ 180, 420, 900 \right\} }$$ n = 180 , 420 , 900 .
