Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要