An alternative way of explaining inconsistencies in a formula is Variable MUSes (VMUSes) [1]. In plain words, a variable MUS of an unsatisfiable formula F is a subset of variables of F, denoted as Var(F), that defines all variables in an unsatisfiable formula and none of its proper subsets is so. In order to define VMUSes, the concept of induced formula is used. Given a formula F, a formula induced by a variable set V is subformula of F, denoted as F|v, and is the following F|v = {c | c ∈ F and Var(c)}. The set F|v is basically the set of clauses from F, that contains only the variables in V.
By using the notions defined above, a subformula F|v of a given F is said to be a VMUS if the following conditions hold:
- F is UnSAT and V ⊆Var(F)
- F|v is unSAT
- For any V' ⊂ V, F|v' is SAT
[1] presents two variations of VMUSes:
- Interesting VMUS (IVMUS)
- Group VMUS (GVMUS)
References
[1] A. Belov, A. Ivrii, A. Matsliah and J. Marques-Silva, On Efficient Computation of Variable MUSes, SAT 2012.
