用约束求解器的证明生成分步解释，提速并保持解释质量。
Using Certifying Constraint Solvers for Generating Step-wise Explanations
- 基于求解器生成的证明构建分步解释框架
- 转换方法使解释序列速度提升显著，质量接近顶尖水平
- 适合需要高效可解释性的约束求解场景
在可解释约束求解领域，通常需向用户说明问题为何无解。近期方法通过生成一系列解释步骤来展示从原始约束中逐步推导出冲突的过程。然而，逐步生成解释计算成本高，限制了其适用范围。本文研究如何利用约束求解器生成的证明作为起点，而非从头计算解释步骤。我们定义了抽象证明框架，使证明与分步解释均可表示其中，并提出多种将证明转换为分步解释序列的方法，重点采用剪枝与简化技术以控制序列长度和步骤复杂度。实验表明，该方法显著加快解释生成速度，且生成的解释质量与当前最优方法相当。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。