Author:

Keywords:

TUPLES - 101070149;info:eu-repo/grantAgreement/EC/HE/101070149, CHAT-Opt - 101002802;info:eu-repo/grantAgreement/EC/H2020/101002802, G070521N#56135703, 46 Information and computing sciences

Abstract:

Debugging unsatisfiable constraint models can be a tedious task. Current tools allow a user to extract a subset of constraints that render the problem unsatisfiable (MUS). However, in some cases, this MUS can be very large or too difficult to understand for a user. We propose to use an existing framework for explaining logic puzzles called step-wise explanations. Applying this framework to unsatisfiable models presents several challenges such as dealing with redundancy in the explanation sequence. To quantify and mitigate this redundancy, we propose several properties good explanation sequences should adhere to, and greedy algorithms supporting these properties. Our results show great improvement in terms of the complexity of explanation sequences, but more elaborate processing of the explanation sequences is only one of the ways explanation sequences can be simplified.