×

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