They say that one picture is worth a thousand words, so I shut up:
Maven, Mercury Maven, Mercury
Sounds familiar Did you guys made progress on explanation when there is no solution?
some.
I do intercept contradictions while building the tree and am working on incorporating explanation function into SAT itself. It will still require interpretation on Mercury side, so I am debating whether explanation belongs to SAT or client. SAT is too formal, so might have to do it in Mercury.