In Minizinc while visualising the execution tree (created via Profile search) I obtain a tree containing gray square.
What do they represent ?
The gray squares are back-jumps. They are parts of the tree for which the solver was able to prove no solution would be present.
In a general constraint programming solver, the solver performs a tree search. Whenever you find that one branch doesn't contain any solutions, you go to another branch. Traditionally, there are two branches for every search decision. For example, a value assignment and its negation. But it is also possible to create a branch for every possible value that the variable can take.
In Lazy Clause Generation solvers, search works a bit differently. Whenever you find that search failed, you let the SAT backend generate a reason, generally referred to as a "no-good". This no-good explains why this branch didn't contain any solutions, and can from then on be enforced as a new constraint. If you just revisit your last decision, then this new constraint might still be violated. Instead, these LCG solvers use a back-jump mechanism to jump up to the last decision where the no-good was not yet violated.