Keep track of justifications/explanations

[sheaf]

As per Vilím's paper Computing Explanations for the Unary Resource Constraint, keeping track of a justification for each constraint propagation would enable more efficient search algorithms, which backtrack only decisions pertaining to the contradiction that was eventually found. This would avoid wasting time searching alternatives when we could have seen in advance that they would lead to contradictions, because they don't affect the underlying reasons that lead to a contradiction.

[sheaf]

This should also allow returning an explanation when a search finds no results.