Loading...
Date
2012
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.
Supervisor
Description
peer-reviewed
Publisher
IOP Publishing
Citation
Journal on Satisfiability, Boolean Modeling and Computation;8, pp. 123-128
Files
Loading...
Belov_2012_MUser.pdf
Adobe PDF, 457.12 KB
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI), FCT