{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T19:12:51Z","timestamp":1662664371010},"reference-count":0,"publisher":"Association for the Advancement of Artificial Intelligence (AAAI)","issue":"7","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAAI"],"abstract":"Certifying the output of tools solving complex problems so as to ensure\nthe correctness of the results they provide is of tremendous importance.\nDespite being widespread for SAT-solvers, this level of exigence has\nnot yet percolated for tools solving more complex tasks, such as model\ncounting or knowledge compilation. In this paper, the focus is laid on a\ngeneral family of top-down Decision-DNNF compilers. We explain how those\ncompilers can be tweaked so as to output certifiable Decision-DNNF\ncircuits, which are mainly standard Decision-DNNF circuits decorated by\nannotations serving as certificates. We describe a polynomial-time\nchecker for testing whether a given CNF\u00a0formula is equivalent or not to\na given certifiable Decision-DNNF circuit. Finally, leveraging a\nmodified version of the compiler d4 for generating certifiable\nDecision-DNNF circuits and an implementation of the checker, we present\nthe results of an empirical evaluation that has been conducted for\nassessing how large are in practice certifiable Decision-DNNF circuits,\nand how much time is needed to compute and to check such circuits.<\/jats:p>","DOI":"10.1609\/aaai.v35i7.16776","type":"journal-article","created":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T18:50:49Z","timestamp":1662663049000},"page":"6244-6253","source":"Crossref","is-referenced-by-count":0,"title":["Certifying Top-Down Decision-DNNF Compilers"],"prefix":"10.1609","volume":"35","author":[{"given":"Florent","family":"Capelli","sequence":"first","affiliation":[]},{"given":"Jean-Marie","family":"Lagniez","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Marquis","sequence":"additional","affiliation":[]}],"member":"9382","published-online":{"date-parts":[[2021,5,18]]},"container-title":["Proceedings of the AAAI Conference on Artificial Intelligence"],"original-title":[],"link":[{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/16776\/16583","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/16776\/16583","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T18:50:50Z","timestamp":1662663050000},"score":1,"resource":{"primary":{"URL":"https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/16776"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,18]]},"references-count":0,"journal-issue":{"issue":"7","published-online":{"date-parts":[[2021,5,28]]}},"URL":"https:\/\/doi.org\/10.1609\/aaai.v35i7.16776","relation":{},"ISSN":["2374-3468","2159-5399"],"issn-type":[{"value":"2374-3468","type":"electronic"},{"value":"2159-5399","type":"print"}],"subject":[],"published":{"date-parts":[[2021,5,18]]}}}