Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
| Autor: | Ivana Černá, Nikola Beneš, Jaroslav Bendík |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Model checking
Theoretical computer science Computer science Computation 020207 software engineering 02 engineering and technology Satisfiability Graph enumeration Constraint (information theory) Set (abstract data type) 0202 electrical engineering electronic engineering information engineering Benchmark (computing) 020201 artificial intelligence & image processing Formal verification |
| Zdroj: | Automated Technology for Verification and Analysis-16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings Lecture Notes in Computer Science Lecture Notes in Computer Science-Automated Technology for Verification and Analysis Automated Technology for Verification and Analysis ISBN: 9783030010898 ATVA |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-030-01090-4_9 |
| Popis: | In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes, algorithms have to test sets of constraints for their simultaneous satisfiability. The type of the test depends on the application domains. The complexity of the tests can be extremely high especially for domains like temporal logics, model checking, or SMT. In this paper, we propose a recursive algorithm that identifies MUSes in an online manner (i.e., one by one) and can be terminated at any time. The key feature of our algorithm is that it minimises the number of satisfiability tests and thus speeds up the computation. The algorithm is applicable to an arbitrary constraint domain. We benchmark our algorithm against the state-of-the-art algorithm Marco on the Boolean and SMT constraint domains and demonstrate that our algorithm really requires less satisfiability tests and consequently finds more MUSes in the given time limits. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|