For loosely constrained problems, yes, constraint programming will enumerate exponential combinations and that's not a good fit for this methodology. The point I was trying to guard against is that the solver isn't smart and therefore when asking, "Is it smart enought to know X?", I'd say it depends.
If the solver in question has some decent bounds propagation on the six or so binary arithmetic constraints in the problem, then no, it won't enumerate all 1001^6 combinations (assuming domains of size 1001).
A more helpful answer from me would have been, "It's unknown if it's smart enough, but the more constrained i.e. the more combinations your constraints reject, the better".
Seeing as there were four solutions out of 1.8 million states (in the domains of size 11 example), that's very constrained.