A Top-Down Compiler for Sentential Decision Diagrams
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Special Track on Knowledge Representation and Reasoning. Pages 3141-3147.
Abstract
The sentential decision diagram (SDD) has been recently proposed as a new tractable representation of Boolean functions that generalizes the influential ordered binary decision diagram (OBDD). Empirically, compiling CNFs into SDDs has yielded significant improvements in both time and space over compiling them into OBDDs, using a bottom-up compilation approach. In this work, we present a top-down CNF to SDD compiler that is based on techniques from the SAT literature. We compare the presented compiler empirically to the state-of-the-art, bottom-up SDD compiler, showing orders-of-magnitude improvements in compilation time.
@inproceedings{ijcai2015p443,
title = {A Top-Down Compiler for Sentential Decision Diagrams},
author = {Oztok, Umut and Darwiche, Adnan},
booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-15}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Qiang Yang and Michael Wooldridge},
pages = {3141--3147},
year = {2015},
month = {7},
note = {Special Track on Knowledge Representation and Reasoning},
url = {https://ijcai.org/proceedings/2015/443},
}
TY - CPAPER TI - A Top-Down Compiler for Sentential Decision Diagrams AU - Oztok, Umut AU - Darwiche, Adnan T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 3141 EP - 3147 UR - https://ijcai.org/proceedings/2015/443 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
