University of Limerick
Browse

On efficient computation of variable MUSes

Download (601.08 kB)
conference contribution
posted on 2012-12-20, 12:33 authored by Anton 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

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC