Arc-consistency closure (source code)

= Arc-consistency closure

The greatest componentwise subdomains of given finite initial <constraint domains> satisfying every directed <arc consistency> condition, allowing empty subdomains. Repeated sound revisions to a fixed point produce this same closure regardless of revision order, provided every affected arc is eventually reconsidered.

For the proof, fix subdomains $E_i$ of the initial $D_i$ satisfying <arc consistency>. If all current $D_i$ contain $E_i$, every value in $E_i$ has a support in $E_j\subseteq D_j$, so revising $i\to j$ preserves $E_i$. <Mathematical induction> shows that every revision preserves every such family $E$. At termination the current domains themselves satisfy <arc consistency>, so they are the greatest such family. Algorithms that stop immediately on the first empty <constraint domain> need not finish computing the closure, but correctly establish that no complete solution exists.