Package mus provides data structures and algorithms for minimal unsatisfiable sets (MUS) in LogicNG.

Package smus provides an algorithm to compute a smallest minimal unsatisfiable set (SMUS) of a set of propositions or formulas in LogicNG.

NewUnsatCore creates a new UnsatCore with the given propositions and the given flag whether the core is guaranteed to be a MUS.

UnsatCore represents an unsatisfiable core of a formula.