ExplanationBackend

Extends ClingoMultishotBackend with functionality to compute Minumal Unsatisfiable Cores (MUC) when there is an UNSAT output.

Examples

• sudoku_advanced

• sudoku_explained

When the domain-control produces an unsatisfiable output this backend will perform subsequents calls to find the subset minimal assumptions that caused the unsatisfiablity. These assuptions not only include those selected by the user, but also can be part of the input. This is needed when some of the input facts also want to be shown to the user. Therefore, this backend adds an argument to the command line: --assumption-signature in which the user can select which signatures will be considered as assumptions in the MUC computation.

Examples

The sudoku_advanced example provides the argument --assumption-signature=initial,3 so that all the initial values of the sudoku are also considered in the unsat core and therefore shown to the user.

attr(pos(X,Y),class,"bg-primary"):-pos(X,Y), not _clinguin_muc(sudoku(X,Y,_)), not _clinguin_muc(initial(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(sudoku(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(initial(X,Y,_)).

The domain-state is then enhanced by the MUC using predicate muc/1.

Examples

In the sudoku, the MUC information will show in red the faulty assumptions.

attr(pos(X,Y),class,"bg-primary"):-pos(X,Y), not _clinguin_muc(sudoku(X,Y,_)), not _clinguin_muc(initial(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(sudoku(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(initial(X,Y,_)).

class ExplanationBackend(args)

Extends ClingoMultishotBackend. This backend will treat an UNSAT result by adding the Minimal Unsatisfiable Core (MUC) to the domain-state, thus allowing the UI to show the faulty assumptions.

clear_assumptions()

Removes all assumptions. Overwrites the parent method by keeping as assumptions the ones provided as input via the command line.

Domain state constructors

The domain state also inclues domain constructors from the parent class.

ExplanationBackend._ds_muc()

Adds information about the Minimal Unsat Core (MUC) Includes predicate _clinguin_muc/1 for every assumption in the MUC It uses a cache that is erased after an operation makes changes in the control.