[Feature] Debugging explanations

[Dekker1]

We discussed two method that can be used to help verify the validity of explanations given by the solver.

Note that in the solver Reason refers to the conjunction that implies a propagation. In this issue I've used the term “explanation” as the clause that could have been added at the root level instead.

Simple

A simple heuristic to protect against typos in the Reason conjunction generated, is to check that all literals are known to be true at this point in time.

In debug builds we could simply check this when propagating.

Harder

When given an explanation R1 /\ R2 /\ ... /\ Rn -> B, negating B would make this clause unsatisfiable in combination with the original constraint being propagated.

One idea is to output the explanations ourself together with the originating constraint, and then check them with a generalized system, such as MiniZinc+gecode.

The same system is employed by CP proof systems to proof correctness of their result. Hopefully we would be able to use the system currently being developed by Emir's team to verify the correctness of our explanations.