|
| << vorige | volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 15 van 16 gevonden artikelen
| Titel: |
Towards efficient MUS extraction |
| Auteur: |
Belov, Anton Lynce, Inês Marques-Silva, Joao |
| Verschenen in: |
AI communications |
| Paginering: | Jaargang 25 (2012) nr. 2 pagina's 97-116 |
| Jaar: |
2012-07-24 |
| Inhoud: |
Minimally Unsatisfiable Subformulas (MUS) find a wide range of practical applications, including product configuration, knowledge-based validation, and hardware and software design and verification. MUSes also find application in recent Maximum Satisfiability algorithms and in CNF formula redundancy removal. Besides direct applications in Propositional Logic, algorithms for MUS extraction have been applied to more expressive logics. This paper proposes two algorithms for computation of MUSes of propositional formulas in Conjunctive Normal Form (CNF). The first algorithm is optimal in its class, meaning that it requires the smallest number of calls to a SAT solver. The second algorithm extends earlier work, but implements a number of new techniques. Among these, this paper analyzes in detail the technique of recursive model rotation, which provides significant performance gains in practice. Experimental results, obtained on representative practical benchmarks, indicate that the new algorithms achieve significant performance gains with respect to state of the art MUS extraction algorithms. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 15 van 16 gevonden artikelen
| << vorige | volgende >> |