Using the DiagnoserNuts And Bolts

TEMPORARY NOTE: The diagnoser is currently (March 2022) disabled. We expect to have it working properly again soon, so watch this space. Meanwhile note that this page does not apply. You can achieve the effect of the “approximate model” tool laboriously by hand, by commenting out sets of constraints and re-solving.

Below the “Solve” and “Check” buttons is another with the label “Diagnose”. This gives access to a tool designed to help you diagnose the errors in your encoding in cases where the syntax check says “OK” but there is no solution.

As an example of a set of constraints with no solution, consider the attempted encoding of the Inconsequential Seminars given on this page. If you click “Solve” you will get the fairly unhelpful error message “No solution found”. What this means logically is that the constraints as we have expressed them, along with the specifications of sorts and vocabulary, are too strong: there is no interpretation of the symbols which makes all of the constraints come out true. Tracking down the incorrect constraint or constraints, however, can be a time-consuming and frustrating business, so the diagnoser is provided. Sometimes it helps!

When you click on “Diagnose”, a box pops up giving you the choice of generating an “approximate model” or an “unsatisfiable core”. An approximate model is an interpretation – an assignment of values to the symbols – which makes almost all of the constraints true. The idea is that since the solver cannot give you a perfect model of your constraints (because there isn’t one) it gives instead the closest one it can find, satisfying as many of the constraints as possible.

In the present case, it manages to find an interpretation which makes everything true except for the claim that the speaker in January is Plodder. Maybe that is the culprit! Well, we examine the English statement of the puzzle, and we find that clue 5 clearly states that the first talk (i.e. in January) is given by Plodder, so that one can’t be false. We can tell the solver that this particular constraint is “hard”, meaning it is not allowed to be violated, by clicking the box next to it in the constraint list to the left of the approximate solution. Now if we demand another approximate model by clicking the “Generate” button, we get one satisfying the hard constraint. This time the unsatisfied constraint is

ALL x (speaker(x) = Madder IMP topic((x + 1)) = Vagueness).

This is part of a longer constraint which wrapped several facts into one formula, and which the solver has decomposed into its constituent clauses. After studying the logic of this formula, we may decide that suspect number 2 is also not guilty, and so mark that long constraint too as hard. On generating yet another approximate model, we get another suggestion: maybe the assertion that vagueness is not the topic in March is incorrect. On searching through the problem description, we find that indeed this is nowhere stated. How did it get into the encoding? – nobody knows! Anyway, this is the error, tracked down in three steps.

The diagnoser also offers to generate an unsatisfiable core. This is a subset of the constraints which has no model although if you remove any one constraint from it you do get a satisfiable set. The logical contradiction preventing solutions from existing must lie within the unsatisfiable core, so something in the core needs to be fixed. In the case of the present example, the unsatisfiable core is not actually very helpful, because 6 clauses are essentially involved in generating the contradiction so the search for the bug is not narrowed down very strongly by the core. If we click on the “Optimal” button, we ask the diagnoser to generate the smallest possible unsatisfiable core (smallest in the sense of containing the smallest number of constraints). In this case, it shows that the 6-constraint core is also the optimal one, so that too does not help much. In other cases, however, there may be a single constraint which contradicts the problem setup all by itself, so in those cases the optimal unsatisfiable core will direct us very precisely to the error.

The diagnosis tool is not a magic bullet. It cannot tell you what you did wrong, since it does not know what you were trying to express, but it can (sometimes) give you useful pointers which may help you to see where the error lies. It is worth knowing that the diagnosis problem is computationally difficult in the worst case, and the optimal diagnosis problem is even harder, as is the problem of generating an optimal approximation to a solution. Therefore the diagnoser may sometimes fail to produce anything useful, especially when the constraint set gets large. That’s not our fault: it’s just the mathematics of the setup!

Anyway, when you get the response “No solution found”, it is generally worth giving the diagnoser a go: if it helps, that’s good; if it doesn’t, well then it doesn’t – at least you lose nothing by asking.