Core-guided minimal correction set and core enumeration

Nina Narodytska, Nikolaj Bjørner, Maria Cristina Marinescu, Mooly Sagiv

Producció científica: Capítol de llibreContribució a congrés/conferènciaAvaluat per experts

35 Cites (Scopus)

Resum

A set of constraints is unsatisfiable if there is no solution that satisfies these constraints. To analyse unsatisfiable problems, the user needs to understand where inconsistencies come from and how they can be repaired. Minimal unsatisfiable cores and correction sets are important subsets of constraints that enable such analysis. In this work, we propose a new algorithm for extracting minimal unsatisfiable cores and correction sets simultaneously. Building on top of the relaxation and strengthening framework, we introduce novel techniques for extracting these sets. Our new solver significantly outperforms several state of the art algorithms on common benchmarks when it comes to extracting correction sets and compares favorably on core extraction.

Idioma originalAnglès
Títol de la publicacióProceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
EditorsJerome Lang
EditorInternational Joint Conferences on Artificial Intelligence
Pàgines1353-1361
Nombre de pàgines9
ISBN (electrònic)9780999241127
DOIs
Estat de la publicacióPublicada - 2018
Publicat externament
Esdeveniment27th International Joint Conference on Artificial Intelligence, IJCAI 2018 - Stockholm, Sweden
Durada: 13 de jul. 201819 de jul. 2018

Sèrie de publicacions

NomIJCAI International Joint Conference on Artificial Intelligence
Volum2018-July
ISSN (imprès)1045-0823

Conferència

Conferència27th International Joint Conference on Artificial Intelligence, IJCAI 2018
País/TerritoriSweden
CiutatStockholm
Període13/07/1819/07/18

Fingerprint

Navegar pels temes de recerca de 'Core-guided minimal correction set and core enumeration'. Junts formen un fingerprint únic.

Com citar-ho