Last week I wrote a post on the effectiveness of using backtracking alone to solve combinatorial problems. It was an interesting exercise to develop the discussion from theory to practice and back to theory again. However, there was a mistake in that development. As pointed by Jean-François Puget in his comment, it is possible to add a small number of symmetry breaking constraints to efficiently refute that class of infeasible instances of the pigeonhole principle used as example. After all, what was actually claimed by the theoretical development that I shortly mentioned is that the refutation of a specific formulation of the problem has an exponential lower-bound. While that could be a case for using a global constraint, it could also be addressed by symmetry breaking.
Symmetries arise naturally in combinatorial problems, but the extent to which they cause concern varies with the solving method used. They matter a lot for backtracking because of their impact in the size of the search space to be explored. We have a formulation with a symmetry breaking constraint if, compared to the formulation without such a constraint, only solutions differing by symmetry from the solutions of the more restricted formulation are feasible for one and not for the other.
There is an intuitive notion that symmetry breaking is a good thing, but care must be taken: what if it makes an easy problem harder? It might be the case that the original problem was underconstrained and additional constraints would rule out exactly the solutions that are easier to find, therefore making the search longer than without them. However, that was not the case of the problem in the previous post and is not likely to be the case in most applications. It is even interesting to ask if there are conditions in which this can be in fact observed.
Nevertheless, symmetry breaking is a bit challenging because it requires taking into account the whole formulation instead of reasoning about each constraint separately. For each symmetry identified in a subproblem, we may come up with an additional constraint that introduces information about the problem context that breaks it. As a consequence, symmetry breaking inference mechanisms cannot be encapsulated within global constraints and we are left with two options: expect good formulations from the modeler or develop some sort of general mechanism to find them.
The current practice is based on the former option, and thus the expertise of the modeler plays an important role in the process. However, the quest for a truly autonomous solver of broader use would demand further advances in the latter possibility. Honestly, I was not aware of the importance of reformulation until thinking about all of this, and it made me look again for Barry O’Sullivan’s paper at AAAI-10 discussing the automation of both modeling and solving. Among recent papers, it is a good start on the topic.
In conclusion, proving that backtracking cannot suffice is a bit trickier that I thought at first. Unless P=NP, there must exist an asymmetrical CSP class (or at least one for which breaking its symmetries would not be an easy problem) with lower-bound refutation asymptotically worst than any polynomial function in the size of the problem. If such a class is yet unknown, the interesting part of looking for it would be to find a number of general inference rules for symmetry breaking that we could use to solve other problems.