A Minimally-Unsatisfiable Core Extractor
By
Zaher Andraus, Yoonna Oh, and Mark Liffiton
University of Michigan, Ann Arbor
Why bother Amuse? | News | Papers | Downloads | Help
Amuse is a fast US extractor. Given an UNSAT CNF instance, it finds a very good approximation for explaining the unsatisfiablity of the instance. Amuse is implemented on top of the Minisat Sat Solver.
[4.26.05] A new beta bytecode release (v0.7)
for Linux is now
available. Please check the Downloads section.
[4.15.04] Hi, Amuse!
Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah and Igor L. Markov, "A Minimally-Unsatisfiable Core Extractor", to appear in DAC 2004, nominated best paper.
Abstract: This paper describes a new algorithm for extracting unsatisfiable subformulas from a given unsatisfiable CNF formula. Such unsatisfiable “cores” can be very helpful in diagnosing the causes of infeasibility in large systems. Our algorithm is unique in that it adapts the “learning process” of a modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. Compared to existing approaches, this method can be viewed as a bottom-up core extraction procedure which can be very competitive when the core sizes are much smaller than the original formula size. Repeated runs of the algorithm with different branching orders yield different cores. We present experimental results on a suite of large automotive benchmarks showing the performance of the algorithm and highlighting its ability to locate not just one but several cores.
Download pdf version.
Contact Zaher Andraus for obtaining the software.
Amuse User Manual: download pdf version.
Contact Zaher Andraus for any questions/comments regarding Amuse.
This page was last updated on 04/26/2005 08:18:09 PM -0400.