Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1673818, author = {Bendík, Jaroslav and Černá, Ivana}, address = {Neuveden}, booktitle = {26th International Conference on Principles and Practice of Constraint Programming}, doi = {http://dx.doi.org/10.1007/978-3-030-58475-7_3}, editor = {Helmut Simonis}, keywords = {Minimal Unsatisfiable Subsets;MUSes;Over-constrained systems}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Neuveden}, isbn = {978-3-030-58474-0}, pages = {37-54}, publisher = {Springer, Cham}, title = {Replication-Guided Enumeration of Minimal Unsatisfiable Subsets}, year = {2020} }
TY - JOUR ID - 1673818 AU - Bendík, Jaroslav - Černá, Ivana PY - 2020 TI - Replication-Guided Enumeration of Minimal Unsatisfiable Subsets PB - Springer, Cham CY - Neuveden SN - 9783030584740 KW - Minimal Unsatisfiable Subsets;MUSes;Over-constrained systems N2 - 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. ER -
BENDÍK, Jaroslav a Ivana ČERNÁ. Replication-Guided Enumeration of Minimal Unsatisfiable Subsets. In Helmut Simonis. \textit{26th International Conference on Principles and Practice of Constraint Programming}. Neuveden: Springer, Cham, 2020, s.~37-54. ISBN~978-3-030-58474-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-58475-7\_{}3.
|