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

• Boolean formula in CNF
• Tolerance parameter $\epsilon >0$
• Confidence parameter $\delta \in (0,1]$

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+\epsilon )$-multiplicative factor of the exact count with confidence at least $1-\delta$

Internals

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

Comments

Tool for approximate counting of minimal unsatisfiable subsets of a given Boolean formula in CNF