Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Using Certifying Constraint Solvers for Generating Step-wise Explanations

Ignace Bleukx, Maarten Flippo, Bart Bogaerts, Emir Demirović, Tias Guns

TL;DR

The paper tackles the computational bottleneck of generating step-wise explanations for unsatisfiable constraint solving. It introduces a general abstract-proof framework that unifies solver proofs (DRCP) and human-oriented explanations, and a pipeline to convert a DRCP proof into concise, user-friendly explanation steps through simplification and MUS-based minimization. Empirical results across Sudoku, Job-shop, and modeling benchmarks show up to ~100x speedups with explanation quality comparable to the current state of the art, enabling scalable explanatory capabilities for certifying solvers. This work enhances practical explainability in constraint solving and points to future work on shorter proofs, solver-guided proof generation, and better handling of auxiliary variables in user explanations.

Abstract

In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable. A recently proposed method for this is to compute a sequence of explanation steps. Such a step-wise explanation shows individual reasoning steps involving constraints from the original specification, that in the end explain a conflict. However, computing a step-wise explanation is computationally expensive, limiting the scope of problems for which it can be used. We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations, instead of computing them step-by-step. More specifically, we define a framework of abstract proofs, in which both proofs and step-wise explanations can be represented. We then propose several methods for converting a proof to a step-wise explanation sequence, with special attention to trimming and simplification techniques to keep the sequence and its individual steps small. Our results show our method significantly speeds up the generation of step-wise explanation sequences, while the resulting step-wise explanation has a quality similar to the current state-of-the-art.

Using Certifying Constraint Solvers for Generating Step-wise Explanations

TL;DR

The paper tackles the computational bottleneck of generating step-wise explanations for unsatisfiable constraint solving. It introduces a general abstract-proof framework that unifies solver proofs (DRCP) and human-oriented explanations, and a pipeline to convert a DRCP proof into concise, user-friendly explanation steps through simplification and MUS-based minimization. Empirical results across Sudoku, Job-shop, and modeling benchmarks show up to ~100x speedups with explanation quality comparable to the current state of the art, enabling scalable explanatory capabilities for certifying solvers. This work enhances practical explainability in constraint solving and points to future work on shorter proofs, solver-guided proof generation, and better handling of auxiliary variables in user explanations.

Abstract

In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable. A recently proposed method for this is to compute a sequence of explanation steps. Such a step-wise explanation shows individual reasoning steps involving constraints from the original specification, that in the end explain a conflict. However, computing a step-wise explanation is computationally expensive, limiting the scope of problems for which it can be used. We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations, instead of computing them step-by-step. More specifically, we define a framework of abstract proofs, in which both proofs and step-wise explanations can be represented. We then propose several methods for converting a proof to a step-wise explanation sequence, with special attention to trimming and simplification techniques to keep the sequence and its individual steps small. Our results show our method significantly speeds up the generation of step-wise explanation sequences, while the resulting step-wise explanation has a quality similar to the current state-of-the-art.

Paper Structure

This paper contains 30 sections, 2 theorems, 2 equations, 4 figures, 7 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Explanations
  3. Proof Logging
  4. Goal: Computing Step-wise Explanations from Proofs
  5. Background
  6. A Framework for Proofs of Unsatisfiability
  7. DRCP as abstract proof
  8. Step-wise explanations as abstract proofs
  9. DRCP-proof to Step-wise explanation
  10. Proof simplification
  11. Simplification over auxiliary variables
  12. Simplification to domain reductions
  13. Solver-level inferences to user-level inferences
  14. Reason minimization
  15. Overview of the proposed methods
  16. ...and 15 more sections

Key Result

Lemma 1

Given a valid proof step $(R, C)$ with $s \in R$, and $\mathit{scope}(C) \subseteq \mathcal{X}$. If $\mathit{sols}_{\mathcal{X}}(c) \subseteq \mathit{sols}_{\mathcal{X}}(s)$, then ${(R \setminus \{s\} \cup \{c\}, C)}$ is a valid proof step.

Figures (4)

  • Figure 1: Overview of the pipeline for generating a step-wise explanation sequence from a proof.
  • Figure 2: Alternative explanation steps for a 4x4 Sudoku
  • Figure 3: Runtime of all methods for different benchmarks
  • Figure 4: Tradeoff of quality vs runtime on all benchmarks.

Theorems & Definitions (18)

  • Definition 1: Minimal Unsatisfiable Subset
  • Definition 2: Abstract proof
  • Definition 3: Atomic Constraint
  • Definition 4: Inference proof step
  • Definition 5: Nogood deriving step
  • Definition 6: Trimmed abstract proof
  • Definition 7: Explanation step
  • Example 1
  • Definition 8: Abstract P-proof
  • Example 2: Removing a step with an auxiliary variable
  • ...and 8 more