Replication-Guided Enumeration of Minimal Unsatisfiable Subsets
| Autor: | Jaroslav Bendík, Ivana Černá |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
050101 languages & linguistics
Theoretical computer science True quantified Boolean formula Computer science 05 social sciences Enumeration algorithm 02 engineering and technology Replication (computing) Satisfiability Set (abstract data type) 0202 electrical engineering electronic engineering information engineering Enumeration 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Boolean satisfiability problem |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030584740 CP |
| DOI: | 10.1007/978-3-030-58475-7_3 |
| Popis: | In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to identify minimal unsatisfiable subsets (MUSes) of F. The more MUSes are identified, the better insight into F’s unsatisfiability is obtained. Unfortunately, finding even a single MUS can be very time consuming since it naturally subsumes repeatedly solving the satisfiability problem, and thus a complete MUS enumeration is often practically intractable. Therefore, contemporary MUS enumeration algorithms tend to identify as many MUSes as possible within a given time limit. In this work, we present a novel MUS enumeration algorithm. Compared to existing algorithms, our algorithm is much more frugal in the number of performed satisfiability checks. Consequently, our algorithm is often able to find substantially more MUSes than contemporary algorithms. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|