cmMUS: A tool for circumscription-based MUS membership testing. This article presents cmMUS-a tool for deciding whether a clause belongs to some minimal unsatisfiable subset (MUS) of a given formula. While MUS-membership has a number of practical applications, related with understanding the causes of unsatisfiability, it is computationally challenging-it is $Sigma_2^P$-complete. The presented tool cmMUS solves the problem by translating it to propositional circumscription, a well-known problem from the area of non-monotonic reasoning. The tool constantly outperforms other approaches to the problem, which is demonstrated on a variety of benchmarks.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Janota, Mikoláš; Marques-Silva, Joao: cmMUS: a tool for circumscription-based MUS membership testing (2011) ioport