Loading...
On efficient computation of variable MUSes
Date
2012
Abstract
In this paper we address the following problem: given an unsatisfiable CNF formula F, find a minimal subset of variables of F that constitutes the set of variables in some unsatisfiable core of F. This problem, known as variable MUS (VMUS) computation problem, captures the need to reduce the number of variables that appear in unsatisfiable cores. Previous work on computation of VMUSes proposed a number of algorithms for solving the problem. However, the proposed algorithms lack all of the important optimization techniques that have been recently developed in the context of (clausal) MUS computation. We show that these optimization techniques can be adopted for VMUS computation problem and result in multiple orders magnitude speed-ups on industrial application benchmarks. In addition, we demonstrate that in practice VMUSes can often be computed faster than MUSes, even when state-of-the-art optimizations are used in both contexts.
Supervisor
Description
peer-reviewed
Publisher
Springer-Verlang
Citation
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012). Lecture Notes in Computer Science;7317, pp. 298-311
Files
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI), FCT