Download PDFOpen PDF in browserEfficiently Explaining CSPs with Unsatisfiable Subset Optimization (Extended Abstract)EasyChair Preprint 87733 pages•Date: September 2, 2022AbstractWe build on a recently proposed method for stepwise explaining solutions of constraint satisfaction problems. An explanation here is a sequence of simple inference steps, where the simplicity of an inference step is measured by the number and types of constraints and facts used, and where the sequence explains all logical consequences of the problem. The explanationgeneration algorithms presented in that work rely heavily on calls for Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a onetoone correspondence between socalled nonredundant explanations and MUSs. The generation of an explanation sequence for a logic grid puzzle ranges from a few minutes to a few hours, which is more than a human would take. Therefore, we build on these formal foundations and tackle the main points of improvement, namely how to efficiently generate explanations that are provably optimal (with respect to the given cost metric). To address this issue, we develop (1) an algorithm based on the hitting set duality for finding optimal constrained unsatisfiable subsets, where `constrainedness' reduces the multiple calls for (optimal) unsatisfiable subsets to a single call; (2) a method for reusing relevant information over multiple calls to these algorithms and; (3) methods exploiting domainspecific information to speedup explanation sequence generation. We experimentally validate our algorithms on a large number of CSP instances. These experiments show that our algorithms outperform the MUS approach both in terms of quality of the explanation and in time to generate it. We show that this approach can be used to effectively find sequences of optimal explanation steps for a large set of constraint satisfaction problems. Keyphrases: Explanation Sequence, Implicit hitting set duality, Unsatisfiable Subset Optimization, constraint satisfaction
