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

Last commit date

2 March 2021

Related papers

https://doi.org/10.1007/978-3-030-53288-8_21

Last publication date

14 July 2020

Related tools

MUS enumeration techniques: MARCO, MCSMUS, UNIMUS

ProVerB specific

View/edit source (Markdown)



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