Finding Minimal Unsatisfiable Subsets (MUSes) of binary constraints is a
common problem in infeasibility analysis of over-constrained systems. However,
because of the exponential search space of the problem, enumerating MUSes is
extremely time-consuming in real applications. In this work, we propose to
prune formulas using a learned model to speed up MUS enumeration. We represent
formulas as graphs and then develop a graph-based learning model to predict
which part of the formula should be pruned. Importantly, our algorithm does not
require data labeling by only checking the satisfiability of pruned formulas.
It does not even require training data from the target application because it
extrapolates to data with different distributions. In our experiments we
combine our algorithm with existing MUS enumerators and validate its
effectiveness in multiple benchmarks including a set of real-world problems
outside our training distribution. The experiment results show that our method
significantly accelerates MUS enumeration on average on these benchmark
problems.

以图形为基础的学习模型加速枚举最小不可满足子集 (MUSes) 的问题，通过对超约束系统的不可行性分析中的公式进行修剪，并且在多个基准测试中验证了方法的有效性。

图剪枝用于枚举最小不可满足子集

Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets

We build on a recently proposed method for stepwise explaining solutions of
Constraint Satisfaction Problems (CSP) in a human-understandable way. An
explanation here is a sequence of simple inference steps where simplicity is
quantified using a cost function. The algorithms for explanation generation
rely on extracting Minimal Unsatisfiable Subsets (MUS) of a derived
unsatisfiable formula, exploiting a one-to-one correspondence between so-called
non-redundant explanations and MUSs. However, MUS extraction algorithms do not
provide any guarantee of subset minimality or optimality with respect to a
given cost function. Therefore, we build on these formal foundations and tackle
the main points of improvement, namely how to generate explanations efficiently
that are provably optimal (with respect to the given cost metric). For that, we
developed (1) a hitting set-based algorithm for finding the optimal constrained
unsatisfiable subsets; (2) a method for re-using relevant information over
multiple algorithm calls; and (3) methods exploiting domain-specific
information to speed up the explanation sequence generation. We experimentally
validated our algorithms on a large number of CSP problems. We found that our
algorithms outperform the MUS approach in terms of explanation quality and
computational time (on average up to 56 % faster than a standard MUS approach).

本研究基于 “最小不可满子集” 算法构建了一种寻找满足给定成本度量的最佳不满足子集的算法，并开发了加速解释序列生成的方法，实验证明，该算法在解释质量和计算时间方面比 “最小不可满子集” 方法更优。