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

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.
Minimal Unsatisfiable Subsets (MUSes)

Links

Repository: https://github.com/jar-ben/exactMUSCounter

Last commit date

26 April 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_15 (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: AMUSIC

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.