Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets

Panagiotis Lymperopoulos, Liping Liu

TL;DR

This work proposes to prune formulas using a learned model to speed up MUS enumeration by developing a graph-based learning model to predict which part of the formula should be pruned.

Abstract

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.

Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets

TL;DR

This work proposes to prune formulas using a learned model to speed up MUS enumeration by developing a graph-based learning model to predict which part of the formula should be pruned.

Abstract

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.
Paper Structure (22 sections, 1 theorem, 9 equations, 3 figures, 3 tables, 1 algorithm)

This paper contains 22 sections, 1 theorem, 9 equations, 3 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Background
  4. Method
  5. CNF formulas as attributed graphs
  6. CNF pruning via graph pruning
  7. Optimization
  8. Loss function:
  9. Learning objective:
  10. Model architecture
  11. Randomized formula generation from problem statistics
  12. Test-time pruning
  13. Experiments
  14. Datasets:
  15. Improving enumeration performance
  16. ...and 7 more sections

Key Result

Proposition 1

Given an unsatisfiable subset $C'\subseteq C$, if $M$ is a MUS of $C'$ then $M$ is a MUS of $C$.

Figures (3)

  • Figure 1: Graph pruning for MUS enumeration. CNF formulas are represented as Literal Clause Graphs and the clause nodes are pruned. The resulting graph is converted back into a formula and MUSes are enumerated. Green denotes two MUSes in the formula. Red denotes clauses that can be pruned without affecting the MUSes. $c_2$ is a critical constraint
  • Figure 2: Extrapolation to larger formulas. Relative (a) and absolute (b) improvement over the base solvers using GRAPE-MUST on formulas of increasing size at a 5-second timeout. Despite the distribution shift, REMUS benefits proportionally more from pruning in formulas up to 200 variables as the smaller size of the pruned formulas accelerates enumeration. MARCO and REMUS maintain a small improvement across all formulas. As indicated by (b) the variance in (a) increases rapidly with formula size as the actual number of MUSes found becomes very small.
  • Figure 3: Comparison between REMUS and GRAPE-MUST+REMUS on hard benchmark problems. Red line indicates equal number of MUSes. Overall GRAPE-MUST enables the discovery of more MUSes.

Theorems & Definitions (3)

  • Definition 1
  • Proposition 1
  • Definition 2