Full dynamic substitutability by SAT encoding

Symmetry in constraint problems can be exploited to greatly improve search performance. A form of symmetry that has been the subject of considerable research is value interchangeability. Automatically detecting full interchangeability is thought to be intractable, so research has focused on either discovery of local interchangeability or programmer knowledge of full interchangeability. This paper shows that full dynamic substitutability can be broken in a CSP by reformulating it as a SAT problem. No analysis is necessary, space requirements are modest, solutions are collected into Cartesian products, and unit propagation enforces forward checking on the CSP. In experiments on unsatisfiable problems, better results are obtained than with standard SAT encodings.