I have started to use choco-solver in my work and didn't understand how propogator and search stradegies interart with each other.
I think choco has some flag that shows me if there is any domain of constraint variables that is changed during propogation. And if there is, then propogation starts again and again until no domain changes occur. And after that, if constraint still not satisfied or fails, search strategies will be connected to solving process.
But output of my progamm shows me that I'm wrong. Propogator really works 2 or 3 times, changing domains each time, but then search strategy is called.
Help me please, where am I wrong in my conclusions? Or it should work just the way I think and there is some mistakes in my code, that lead to wrong output?
Sorry for my bad english
Choco is a Constraint Programming solver, these solvers all work according to the same principe.
Different than a brute force search, a constraint solver will first call all (relevant) propagators to remove values, from the variable domain, that it knows the variables can't take. Calling one propagator might trigger new values to become impossible and might thus trigger other propagators to run again.
Once all propagators report that they can't remove anymore values (we call this fix point), the search strategy will be consulted to see what to do next. (In general this is a guess to what should be a solution and we might need to backtrack).
If all variables have only one possible value, this is a solution. However, it can happen that in our search a variable loses all its possible values. In this case a propagator will fail. If we had already used search, we will need to backtrack. If this was at the root node, then it means the problem was unsatisfiable.
For more information, try the tutorials of several constraint solvers. A lot of them can be found on Wikipedia. You might also be able to find online courses.