On the tractable counting of theory models and its application to belief revision and truth maintenance
| dc.creator | Darwiche, Adnan | |
| dc.date | 2000-03-09 | |
| dc.date.accessioned | 2026-07-07T03:16:02Z | |
| dc.date.available | 2026-07-07T03:16:02Z | |
| dc.description | We introduced decomposable negation normal form (DNNF) recently as a tractable form of propositional theories, and provided a number of powerful logical operations that can be performed on it in polynomial time. We also presented an algorithm for compiling any conjunctive normal form (CNF) into DNNF and provided a structure-based guarantee on its space and time complexity. We present in this paper a linear-time algorithm for converting an ordered binary decision diagram (OBDD) representation of a propositional theory into an equivalent DNNF, showing that DNNFs scale as well as OBDDs. We also identify a subclass of DNNF which we call deterministic DNNF, d-DNNF, and show that the previous complexity guarantees on compiling DNNF continue to hold for this stricter subclass, which has stronger properties. In particular, we present a new operation on d-DNNF which allows us to count its models under the assertion, retraction and flipping of every literal by traversing the d-DNNF twice. That is, after such traversal, we can test in constant-time: the entailment of any literal by the d-DNNF, and the consistency of the d-DNNF under the retraction or flipping of any literal. We demonstrate the significance of these new operations by showing how they allow us to implement linear-time, complete truth maintenance systems and linear-time, complete belief revision systems for two important classes of propositional theories. | |
| dc.identifier | https://arxiv.org/abs/cs/0003044 | |
| dc.identifier | http://arxiv.org/abs/cs/0003044 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/30204 | |
| dc.subject | Artificial Intelligence | |
| dc.subject | I.2.3 | |
| dc.title | On the tractable counting of theory models and its application to belief revision and truth maintenance | |
| dc.type | text |