## cmMUS

 swMATH ID: 9773 Software Authors: Janota, Mikoláš; Marques-Silva, Joao Description: 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. Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-20895-9_30 Related Software: Referenced in: 0 Publications