Using Certifying Constraint Solvers for Generating Step-wise Explanations

• URL: http://arxiv.org/abs/2511.10428v1
• Date: Fri, 14 Nov 2025 01:50:58 GMT
• Title: Using Certifying Constraint Solvers for Generating Step-wise Explanations
• Authors: Ignace Bleukx, Maarten Flippo, Bart Bogaerts, Emir Demirović, Tias Guns,
• Abstract summary: We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations.<n>We then propose several methods for converting a proof to a step-wise explanation sequence.<n>Our results show our method significantly speeds up the generation of step-wise explanation sequences.
• Score: 8.26913199549645
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Exploiting Constraint Reasoning to Build Graphical Explanations for Mixed-Integer Linear Programming [0.6749750044497732]
  X-MILP is a domain-agnostic approach for building contrastive explanations for MILPs.<n>First, we show how to encode the queries a user makes about the solution of an MILP problem as additional constraints.<n>Then, we determine the reasons that constitute the answer to the user's query by computing the Irreducible Infeasible Subsystem (IIS)
  arXiv  Detail & Related papers  (2025-07-17T11:25:33Z)
• Reverse em-problem based on Bregman divergence and its application to classical and quantum information theory [53.64687146666141]
  Recent paper introduced an analytical method for calculating the channel capacity without the need for iteration. We turn our attention to the reverse em-problem, proposed by Toyota. We derive a non-iterative formula for the reverse em-problem.
  arXiv  Detail & Related papers  (2024-03-14T10:20:28Z)
• Explanation Selection Using Unlabeled Data for Chain-of-Thought Prompting [80.9896041501715]
  Explanations that have not been "tuned" for a task, such as off-the-shelf explanations written by nonexperts, may lead to mediocre performance. This paper tackles the problem of how to optimize explanation-infused prompts in a blackbox fashion.
  arXiv  Detail & Related papers  (2023-02-09T18:02:34Z)
• Synthetic Prompting: Generating Chain-of-Thought Demonstrations for Large Language Models [121.54462976635743]
  Large language models can perform various reasoning tasks by using chain-of-thought prompting, which guides them to find answers through step-by-step demonstrations. We introduce Synthetic prompting, a method that leverages a few handcrafted examples to prompt the model to generate more examples by itself. We evaluate our method on numerical, symbolic, and algorithmic reasoning tasks, and show that it outperforms existing prompting techniques.
  arXiv  Detail & Related papers  (2023-02-01T17:33:12Z)
• Learning to Reason With Relational Abstractions [65.89553417442049]
  We study how to build stronger reasoning capability in language models using the idea of relational abstractions. We find that models that are supplied with such sequences as prompts can solve tasks with a significantly higher accuracy.
  arXiv  Detail & Related papers  (2022-10-06T00:27:50Z)
• Learning to Reason Deductively: Math Word Problem Solving as Complex Relation Extraction [10.721488421356053]
  Solving math word problems requires deductive reasoning over the quantities in the text. Recent research efforts mostly relied on sequence-to-sequence or sequence-to-tree models to generate expressions. We propose a novel approach that presents explainable deductive reasoning steps to iteratively construct target expressions.
  arXiv  Detail & Related papers  (2022-03-19T12:37:16Z)
• Counterfactual Explanations in Sequential Decision Making Under Uncertainty [27.763369810430653]
  We develop methods to find counterfactual explanations for sequential decision making processes. In our problem formulation, the counterfactual explanation specifies an alternative sequence of actions differing in at most k actions. We show that our algorithm finds can provide valuable insights to enhance decision making under uncertainty.
  arXiv  Detail & Related papers  (2021-07-06T17:38:19Z)
• Efficiently Explaining CSPs with Unsatisfiable Subset Optimization [17.498283247757445]
  We build on a recently proposed method for 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. We tackle two emerging questions, namely how to generate explanations that are provably optimal and how to generate them efficiently.
  arXiv  Detail & Related papers  (2021-05-25T08:57:43Z)
• Discrete Reasoning Templates for Natural Language Understanding [79.07883990966077]
  We present an approach that reasons about complex questions by decomposing them to simpler subquestions. We derive the final answer according to instructions in a predefined reasoning template. We show that our approach is competitive with the state-of-the-art while being interpretable and requires little supervision.
  arXiv  Detail & Related papers  (2021-04-05T18:56:56Z)
• Conditional gradient methods for stochastically constrained convex minimization [54.53786593679331]
  We propose two novel conditional gradient-based methods for solving structured convex optimization problems. The most important feature of our framework is that only a subset of the constraints is processed at each iteration. Our algorithms rely on variance reduction and smoothing used in conjunction with conditional gradient steps, and are accompanied by rigorous convergence guarantees.
  arXiv  Detail & Related papers  (2020-07-07T21:26:35Z)
• A framework for step-wise explaining how to solve constraint satisfaction problems [21.96171133035504]
  We study the problem of explaining the inference steps that one can take during propagation, in a way that is easy to interpret for a person. Thereby, we aim to give the constraint solver explainable agency, which can help in building trust in the solver.
  arXiv  Detail & Related papers  (2020-06-11T11:35:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.