PV1 ⊧ CountMUSTcounts minimal unsatisfiable subsets of a given boolean formula

Exact minimal unsatisfiable subset (MUS) counter that does not rely on exhaustive enumeration.

Application domain/field

• Minimal Unsatisfiable Subsets (MUSes)
• MUS counting

Type of tool

MUS counter

Expected input

Unsatisfiable set F of Boolean clauses (i.e. a Boolean formula in CNF)

Format:

If it is a "Plain" MUS then DIMACS .cnf format If it is a "group" MUS then a .gcnf file for a "group DIMACS format". More detail about the input format is available in the README of the repository.

Expected output

Number of Minimal Unsatisfiable Subsets (MUSes) of F.

Internals

Uses GANAK, RIME and UWrMaxSat.