You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

MUSer2: An Efficient MUS Extractor1

Subtitle: System description

Article type: Research Article

Authors: Belov, Antona | Marques-Silva, Joaoa; b

Affiliations: [a] CASL/CSI, University College Dublin, Dublin, Ireland. E-mails: anton.belov@ucd.ie, jpms@ucd.ie | [b] IST/INESC-ID, Lisbon, Portugal

Note: [1] This work is partially supported by SFI grant BEACON (09/IN.1/I2618), and by FCT grants ATTEST (CMU-PT/ELE/0009/2009) and POLARIS (PTDC/EIA-CCO/123051/2010).

Keywords: Minimal unsatisfiability, MUS extraction, SAT applications

DOI: 10.3233/SAT190094

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 123-128, 2012

Received 1 June 2012
|
Revision received 1 August 2012
|
Published: 1 December 2012
Get PDF open access

Abstract

Algorithms for extraction of Minimally Unsatisfiable Subformulas (MUSes) of CNF formulas find a wide range of practical applications, including product configuration, knowledge-based validation, hardware and software design and verification. This paper describes the MUS extractor MUSer2. MUSer2 implements a wide range of MUS extraction algorithms, integrates a number of key optimization techniques, and represents the current state-of-the-art in MUS extraction.

Show more