Using Certifying Constraint Solvers for Generating Step-wise Explanations

AI summary

Overview

Research area: Explainable Constraint Solving / Constraint Programming, specifically the intersection of proof logging (certifying algorithms) and user-facing explanations for unsatisfiable constraint satisfaction problems (CSPs).

Technical level: Advanced. The paper assumes familiarity with constraint satisfaction, propagation, proofs of unsatisfiability, and MUS (Minimal Unsatisfiable Subset) computation, and it presents formal definitions of abstract proofs.

Scope: The paper proposes a framework that represents both solver-generated unsatisfiability proofs (in the DRCP format) and human-oriented step-wise explanation sequences as instances of "abstract proofs," and uses this shared representation to convert a proof into a step-wise explanation far faster than existing methods.

What This Paper Is About

When a constraint solver reports that a problem has no solution, users need an explanation they can understand. A popular approach is a step-wise explanation: a sequence of small reasoning steps, each combining a few of the user's own constraints, that together explain the conflict. Computing these sequences is currently very expensive because it requires repeated calls to an NP-oracle at every step. This paper asks whether a proof that a certifying solver already produces during solving can instead be reused and transformed into a step-wise explanation, avoiding that step-by-step cost.

Key Contributions

1. A general framework of abstract proofs: The authors define an abstract proof as a sequence of pairs (R_i, C_i), where C_i is a set of derived constraints and R_i the reasons for them, with the validity condition R_i ⊧ C_i and R_i ⊆ C ∪ ⋃_{1≤j<i} C_j. They show that both DRCP-format solver proofs and step-wise explanation sequences are instances of this framework, differing in the type of reasons used (solver-level vs. user-level constraints) and the type of constraints derived (disjunction vs. conjunction).

2. A suite of proof-transformation techniques: They propose proof simplification over auxiliary variables, simplification to domain reductions, replacement of solver-level inferences with user-level constraints, and reason minimization, all combined into a pipeline.

3. A reason-minimization algorithm: Algorithm 1 (MinimizeReasons) traverses the proof from back to front, tracking a set of required reasons (Req), discarding unneeded steps, and computing a subset-minimal set of reasons per step using an MUS call. It supports two modes: local (only the step's given reasons are candidates) and global (all user-level constraints and previously derived constraints are candidates).

4. An experimental evaluation across three benchmark families, showing speedups of approximately 100x with minimal processing and at least 10x with the slowest variant relative to the state-of-the-art SimplifyGreedy method, while keeping explanation quality similar.

Main Findings

• Large speedup with minimal processing: On the Sudoku and Job-shop benchmarks, the approach with minimal post-processing (Trim) finds a step-wise explanation approximately 100x faster than SimplifyGreedy. The Trim approach requires no NP-reasoning after the solver produces the proof, because the DRCP format lists each step's reasons explicitly.

• Slowest variant is still much faster: For all benchmarks, even the slowest method tested (Min. glob + Min. loc) finds an explanation sequence at least 10 times faster than the state of the art.

• State of the art fails on some instances: In the Modeling examples benchmark, SimplifyGreedy could not find a step-wise explanation for all instances, running out of time (1 hour) or memory for 29 of the 102 instances.

• Local minimization is faster than global: For example in the Sudoku benchmark, Trim + Min. loc finds an explanation sequence around 5-10 times faster than Trim + Min. glob, since global minimization must consider many more candidate reasons.

• Minimizing after domain-reduction simplification is faster: It is generally faster to apply minimization after the proof has been simplified to only contain domain reductions, because the proof is shorter at that point.

• Trim produces the most complex explanations: In the Job-shop benchmark, Trim needs on average 2.7 constraints in its most difficult step, whereas all other methods achieve a single constraint per step. For Sudoku and Modeling examples, Trim needs on average 7.5 and 3.5 constraints respectively in its most difficult step.

• Best quality-runtime trade-off: Trim + Min. glob produces explanation sequences of similar quality to SimplifyGreedy at significantly lower runtime. On Sudoku, SimplifyGreedy still finds smaller steps on average (average max step size 1.2 versus 3.4 for Trim + Min. glob), meaning some facts are easier to explain than those listed in the DRCP proof.

• Outliers drive average complexity for Sudoku: The higher average complexity of Trim + Min. glob on Sudoku is mainly due to outliers; for more than half of the explanation sequences it produces sequences with only a single constraint in each proof step.

• Trim's average sequence lengths: Job-shop 24.3 steps (±7.9, median 25.0), Sudoku 85.9 steps (±37.4, median 90.0), Modeling examples 11.5 steps (±17.6, median 5.0).

Methodology in Plain English

The authors start from the observation that a certifying constraint solver can already emit a machine-checkable proof of unsatisfiability in the DRCP format, and that this proof is essentially a chain of small reasoning steps. They define a common formal language, "abstract proofs," in which both such proofs and human-oriented explanation sequences can be written down, then describe how to translate between them.

The translation pipeline works as follows. First, solve the problem and parse the proof. Second, transform the proof to the user's level by removing every step whose derived constraint involves auxiliary variables introduced by the modeling system. Third, replace solver-level constraints appearing as reasons with the user-level constraints they came from. Fourth, trim redundant steps. Fifth, remove steps that derive intermediate constraints over multiple variables, keeping only domain reductions. Finally, merge steps that share the same reasons and print the explanation sequence.

Optionally, extra minimization can be inserted, using an MUS algorithm to find subset-minimal reason sets for each step, in either a local or global mode. The authors compare these variants on three benchmark families: 100 unsatisfiable Sudoku instances, 100 unsatisfiable job-shop instances (limited makespan), and 102 example models drawn from the CPMpy and CSP-lib repositories that were altered to contain a modeling error such as an off-by-one error or a swapped comparison. They implement the approach in Python 3.11 with CPMpy v0.9.24, use the Pumpkin LCG-solver (commit d730b05) to generate proofs, use the SMUS algorithm with Exact v2.1.0 as SAT-oracle and Gurobi v.12.0.1 as hitting set solver for MUSes, and run on a single core of an Intel Xeon Silver 4514Y with 8GB RAM. Results are compared against SimplifyGreedy (Bleukx et al. 2023), the current state of the art.

Why This Matters

Impact on research: The work bridges two research lines that had been separate—proof logging for solver trustworthiness and explanation generation for constraint solving. By using a proof the solver already produces, it removes the repeated NP-oracle calls that bottlenecked step-wise explanation, opening the door to explaining much larger unsatisfiable models. The abstract-proof framework also gives a common vocabulary for reasoning about machine-verifiable proofs and human-interpretable explanations together.

Real-world applications:

• Diagnosing infeasible scheduling and planning models, such as the job-shop models studied here, where a limited makespan makes the model unsatisfiable.
• Debugging faulty constraint models written by users, which is precisely the setting of the Modeling examples benchmark where errors like off-by-one mistakes or swapped comparisons were introduced.
• Explaining infeasible configurations or resource allocations in declarative solvers used inside larger software systems.
• Educational tools that walk a learner through a puzzle or logic problem step by step, building on the original Sudoku/logic-puzzle motivation of the step-wise explanation framework.

Industry relevance: Solver-generated certificates are important because reports exist of solvers returning faulty answers (Brummayer and Biere 2009). Since proof logging is already being adopted in SAT (DRAT), MaxSAT, pseudo-Boolean optimization, and CP, companies already paying the cost of producing proofs can reuse them to obtain user-facing explanations at little additional computational cost—the minimal pipeline adds no NP-reasoning at all.

Future Directions

• Shorter proofs for smaller explanations: The authors propose finding shorter proofs (citing Sidorov et al. 2024) or adapting solver behavior so it produces proofs that are better suited to being transformed into step-wise explanations.

• Better use of proof theory: They suggest drawing more inspiration from proof logging and proof-theory to improve the explanation itself, not just its computation.

• Integrating auxiliary variables into user-level explanations: Auxiliary variables are currently removed because they do not fit the step-wise explanation framework, but the authors note they could be useful for compressing the overall proof. How to integrate them into a user-level explanation remains open and challenging, since modeling systems can introduce them in many different ways.

• Extending the approach to larger problems: The authors state their methods can now be applied to larger problems for which existing algorithms would be unthinkable, implying further scaling and evaluation is a natural next step.

Target Audience

This paper is aimed at researchers and graduate students in constraint programming, automated reasoning, and explainable AI, particularly those working on explanations of unsatisfiability, MUS extraction, or proof logging. It is also relevant to practitioners who build constraint models in tools such as MiniZinc or CPMpy and need to understand why a model is infeasible, and to developers of certifying solvers who want to turn the proofs their solvers already emit into human-facing output. The formal definitions and MUS-based algorithms make the paper most accessible to readers already comfortable with constraint satisfaction and SAT-based reasoning.

Authors’ 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.