Certifying Top-Down Decision-DNNF Compilers
Type de document :
Communication dans un congrès avec actes
Titre :
Certifying Top-Down Decision-DNNF Compilers
Auteur(s) :
Capelli, Florent [Auteur]
Linking Dynamic Data [LINKS]
Lagniez, Jean-Marie [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]
Marquis, Pierre [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]
Institut Universitaire de France [IUF]
Linking Dynamic Data [LINKS]
Lagniez, Jean-Marie [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]
Marquis, Pierre [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]
Institut Universitaire de France [IUF]
Titre de la manifestation scientifique :
AAAI 2021 - 35th Conference on Artificial Intelligence
Ville :
Virtual
Pays :
France
Date de début de la manifestation scientifique :
2021-02-02
Discipline(s) HAL :
Informatique [cs]/Intelligence artificielle [cs.AI]
Résumé en anglais : [en]
Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SATsolvers, this level of exigence has not yet ...
Lire la suite >Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SATsolvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler D4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are the certifiable Decision-DNNF circuits that can be generated in practice, and how much time is needed to compute and to check such circuits.Lire moins >
Lire la suite >Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SATsolvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler D4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are the certifiable Decision-DNNF circuits that can be generated in practice, and how much time is needed to compute and to check such circuits.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Projet ANR :
Collections :
Source :
Fichiers
- https://hal.inria.fr/hal-03111679/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-03111679/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-03111679/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- certifator-aaai21.pdf
- Accès libre
- Accéder au document