Generalised Arc Consistency via the Synchronised Product of Finite Automata wrt a Constraint
Nicolas Beldiceanu
TL;DR
The paper tackles a matrix CSP where each row must satisfy a DFA and each column obeys a shared constraint, by employing a synchronised product of automata to propagate GAC. It shows how the resulting automaton can be reformulated into a Berge-acyclic conjunction of one regular constraint and n table constraints, enabling efficient propagation and early infeasibility proofs. The authors then extract minimal solutions from the automaton and solve small MIP models to enforce capacity/demand constraints, demonstrating strong practical performance on a Hydrogen Distribution Problem with small automata and rapid optimality proofs. The approach is particularly effective when the number of rows is modest and the column constraint is tight, and it opens avenues for extension via MDDs for heterogeneous column constraints.
Abstract
Given an $m$ by $n$ matrix $V$ of domain variables $v_{i,j}$ (with $i$ from $1$ to $m$ and $j$ from $1$ to $n$), where each row $i$ must be accepted by a specified Deterministic Finite Automaton (DFA) $\mathcal{A}_i$ and each column $j$ must satisfy the same constraint $\texttt{ctr}$, we show how to use the \emph{synchronised product of DFAs wrt constraint} $\texttt{ctr}$ to obtain a Berge-acyclic decomposition ensuring Generalised Arc Consistency (GAC). Such decomposition consists of one \texttt{regular} and $n$ \texttt{table} constraints. We illustrate the effectiveness of this method by solving a hydrogen distribution problem, finding optimal solutions and proving optimality quickly.