Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (Extended Abstract)

EasyChair Preprint 8773

Abstract

We build on a recently proposed method for step-wise 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 explanation-generation algorithms presented in that work rely heavily on calls for Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called non-redundant 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 re-using relevant information over multiple calls to these algorithms and; (3) methods exploiting domain-specific information to speed-up 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

@booklet{EasyChair:8773,
  author    = {Emilio Gamba and Bart Bogaerts and Tias Guns},
  title     = {Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (Extended Abstract)},
  howpublished = {EasyChair Preprint 8773},
  year      = {EasyChair, 2022}}