PV1 AMUSIC: Approximate Minimal Unsatisfiable Subsets Implicit Countercounts minimal unsatisfiable subsets of a given formula in CNF

Application domain/field

Minimal unsatisfiable sets (MUSes)

Type of tool

Counting tool?

Expected input

Format:

A .gcnf or .cnf file for the boolean formula. The tolerance and confidence parameter can be set with arguments given to the script.

Expected output

Estimate of the amount of MUSes guaranteed to be within (1+ε)-multiplicative factor of the exact count with confidence at least 1δ

Internals

Uses CAQE, CADET, QRATPre+, muser2, UWrMaxSat, pysat

Comments

Tool for approximate counting of minimal unsatisfiable subsets of a given Boolean formula in CNF
Minimal Unsatisfiable Subsets (MUSes)

Links

https://github.com/jar-ben/amusic

Related papers

Approximate Counting of Minimal Unsatisfiable Subsets

Last publication date

14 July 2020

Related tools

MUS enumeration techniques: MARCO, MCSMUS, UNIMUS

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.