posted on 2012-12-20, 12:33authored byAnton Belov, Alexander Ivrii, Arie Matsliah, Joao Marques-Silva
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.
History
Publication
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012). Lecture Notes in Computer Science;7317, pp. 298-311
Publisher
Springer-Verlag
Note
peer-reviewed
Other Funding information
SFI, FCT
Rights
The original publication is available at www.springerlink.com