Coming Back to MUSes and MSSes...
The computation of minimal unsatisfiable subformulas attracted a lot of interest in the recent years. There are several motivations behind this increased interest. First, the complexity (e.g. size) of problems solved by SAT solvers increased a lot recently. For instance, abstraction-refinement model checkers need better abstractions that will help speed up the process. Second, understanding the reasons of conflicts/inconsistencies in a CNF formula requires concise descriptions that are comprehensible by developers. Third, similar to relationship between explanations and relaxations of CSP problems, there is a duality between MUSes and maximally satisfiable subformulas (MSS) and this duality avails the (possible) uses of MSSes. A detailed overview is provided in [1] and [2].
Given a CNF formula F, a minimal unsatisfiable subformula C is a subset of clauses from F (C ⊆ F) that is unsatisfiable and removal of a clause c from C makes C \ {c} satisfiable. The minimum unsatisfiable subformula is one such subformula that has minimum cardinality. The computation of minimum unsatisfiable subformula is given as ∑
2-complete in [3]. An important point here related to computation of MUSes from
MSSes, in an analogy to computation of explanations from relaxations as discussed in the previous post, is
the following from [1]: because computing SAT is in NP (i.e. relatively
easy) and UnSAT is CoNP, MSSes are computed first....
However, in general it is not enough to obtain one MUS to explain inconsistencies as there might be many of them. Moreover, the number of clauses contained in a MUS (i.e. inconsistency explanation) can be large leading to a situation the developer can not comprehend or can not understand the reason accurately. Thus several variations of MUS computations have been proposed to make MUSes more concise. I will discuss two of them in here leaving some others to future posts. The first one has been introduced in [1], optimized in [4] and [5]. We will call High-level MUS in what follows. The second one is presented in [6] and we will call it Variable MUS.
High-level MUSes
I am going to discuss High-Level MUSes here with a chronological approach, i.e. towards most recent paper...
[1] In some applications of SAT such as model checking and formal equivalence verification (FEV), MUSes are usually low-level projections (are generated from) of some high-level statements written in a more expressive (and presumably more compact) notation such as first-order logic. Thus one is interested in finding MUSes that are closer to these high-level statements. In order to explain how High-level MUSes are obtained, we first need to explain the concept "selector-variable". A boolean variable v is a selector variable that implies a clause C,
v → C (i.e. -v ∨ C). It can be used to enable (by assigning
true) or disable (by assigning
false) the clause C.
By using selector variables we can identify each clause or group them. In particular, the set of clauses that are associated with the same high-level statement can be marked with the same selector variable. Given a set of clauses {c1,c2,c3,c4} and a set of selector variables F={v1,v2}, consider the following CNF encoding:
-v1 ∨ c1
-v2 ∨ c2
-v2 ∨ c3
-v1 ∨ c4
This encoding can effectively associate {c1,c4} with v1 and {c2,c3} with v2.
[2] focuses on finding one high-level MUS even though the approach can be used for standard MUS extraction. It provides two algorithms: resolution-based MUS extraction and selector-variable based MUS extraction. In general the algorithm first finds a clause-level non-minimal unsatisfiable subformula that contains a part of a projection of an interesting clause (i.e. an equisatisfiable formula obtained by Tseitin transformation) and then tries to squeeze it to minimal. I won't provide the details of algorithms but just present the High-Level MUS definition in the paper. Given a formula
F = f1 ∧ f2 ... ∧ fn where each f is a propositional formula and a propositional formula R
(called remainder)
, a high-level MUS, denoted as
UC(F,R), imply the following conditions:
-
F ∧ R is UnSAT,
- it is a subset of F, i.e.
UC(F,R) ⊆ F
-
UC(F,R) ∧ R is UnSAT
Here each f ∈ F is called an interesting constraint.
In the next post, I will discuss Variable MUSes...
References:
[1] Mark H. Liffiton and Karem A. Sakallah, "Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints", Journal of Automated Reasoning, 2008
[2] Éric Grégoire, Bertrand Mazure, Cédric Piette, "On Approaches to Explaining Infeasibility of Sets of Boolean Clauses", 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2008
[3] Anupam Gupta, "Learning Abstractions for Model Checking", PhD Thesis, CMU, 2006
[4] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction", Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design
[5] V. Ryvchinm, O. Strichman, "Faster Extraction of High-Level Minimal Unsatisfiable Cores", Proceedings of the 14th international conference on Theory and application of satisfiability testing (SAT), 2011.
[6] A. Belov, A. Ivrii, A. Matsliah, J. Marques-Silva, "On efficient computation of variable MUSes", Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing(SAT), 2011.
