|
|
About MiniUnsat and its algorithm
Hans van Maaren and Siert Wieringa, Finding guaranteed MUSes fast, H. Kleine Büning and X. Zhao (Eds.): SAT2008, LNCS 4996, pp. 291-304, Springer, Heidelberg (2008).
Presentation slides as used in the SAT2008 conference:
- As PPT - For Microsoft Powerpoint
- As PDF - Without the animations on slides 7 and 12
Note
Definition 1 and proposition 1 in the publication, as well as slide 6 of the presentation slides state that:
- Definition 1 - A critical clause of an unsatisfiable formula F is a clause that belongs to every unsatisfiable subset of the formula F.
- Proposition 1 - In a MUS every clause is a critical clause.
The proposition seems to confuse some people, who will claim it can not be true as there are formulas that contain two disjunct causes of unsatisfiability and therefore do not contain any critical clause. First of all, definition 1 does not state that no such formula exists. Second, critical clause in proposition 1 refers to critical for the unsatisfiability of the MUS itself. Obviously there are no guarantees that those clauses are also critical for the unsatisfiability of some larger formula the MUS might have been extracted from.
|
|
