Unsatisfiability Error Messages

Unsatisfiability Error Messages

Owner: @johntyree

This page is for gathering and testing out ideas for recovering good error messages from failed solver runs.

The fragility of the current solution is tracked in https://github.com/enthought/sat-solver/issues/142. If this results in a robust technique for putting together informative error messages that aren't overwhelming, please go close that issue.

---

When the sat-solver terminates unsuccessfully, we're left with three things.

• Conflict clause: The clause we were looking at when we discovered that we needed to backtrack but had no options left.
• Learned clause: The new clause derived from attempting to backtrack away from the conflict clause.
  • This has a trail of clauses attached to it which should include the conflict clause.
  • This should consist of exactly one literal which is opposite to what has already been assigned to the id. I.e., if we've assigned True to id 4, then this clause will be (-4,).

If we extract the literal (the "implicand") in the learned clause, we can look it up in our dict of id -> assigning clause to find the clause that led to its assignment. My current understanding is that if for some reason the solver had come to this conflict from the opposite direction, this "implicand clause" would be the conflict clause and vice versa.

---

Implementation #1 (CURRENT)

• Get all "interesting" clauses by taking the conflict clause, learned clause, and the implicand clause, flattening out any learned clauses by replacing them with their clause trails.
• Then searching this set for clauses with RuleType.job_* rules. These are the rules that came straight from the user.
• Find the shortest paths connecting each pair of these job clauses, if it exists.
• Filter that list of paths down to just the paths which have the greatest number of job clauses in it. There may be more than one.
  • An alternative might be to find a minimal set of paths that include all of the end points that are part of any path.
• Starting with the shortest paths, filter out paths which do not include any clauses that have not already been seen in a previous path.

This should produce a short, unique path for each conflict we've bumped into during the failure. In the normal case, this will just be a single path, but in the case of multi-way conflicts, it might be more than one.

Implementation #2 (PROPOSED)

This should work just like #1 except that we find all shortest paths between conflicting requirements.

For example if We want to install A0, which depends on B0 and B1, as well as D0, which conflicts with B0 and B1 then we show both failing paths, not just B1, which is what we are most likely to do now.