linear in the size of the original d-NNF**. It is easy to check that the result is equivalent to** the negation of the given d-NNF **sentence and is also in** d-NNF.

- sd-DNNF and d-DNNF**. Unknown.**
- MODS**. Σ =** Vn i=1 xi **has only one model over** Sn i=1{xi} but its negation ¬**Σ has 2**n − 1 models over Sn i=1{xi}**. Hence** MODS **cannot satisfy** ¬C. ✷

## References

A. Cimmati, E. Giunchiglia, F. G., & Traverso, P. (1997). Planning via model checking: a decision procedure for AR. In **Proceedings of the** 4 th European Conference on Planning (ECP'97)**, pp.**
130–142.

Blum, M., Chandra, A. K., & Wegman, M. N. (1980). Equivalence of free Boolean **graphs can be**
decided probabilistically in polynomial time. Information Processing Letters, 10 **(2), 80–82.**
Boole, G. (1854). An investigation of the laws of thought**. Walton and Maberley, London.** Boufkhad, Y., Gr´egoire, E., Marquis, P., Mazure, B., & Sa¨ıs, L. (1997). **Tractable cover compilations.**
In Proc. of the 15th International Joint Conference on Artificial Intelligence (IJCAI'97)**, pp.**
122–127, Nagoya.

Bryant, R. E. (1986). Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35**, 677–691.**
Bryant, R. E. (1992). Symbolic Boolean manipulation with ordered binary decision diagrams. ACM
Computing Surveys, 24 **(3), 293–318.**
Cadoli, M., & Donini, F. (1997). A survey on knowledge compilation. **AI Communications**, 10, 137–150. (printed in 1998).

Cadoli, M., Donini, F., Liberatore, P., & Schaerf, M. (1996). Comparing space efficiency of propositional knowledge representation formalisms. In **Proc. of the** 5 rd **International Conference on**
Knowledge Representation and Reasoning (KR'96)**, pp. 364–373.**
Chandra, A., & Markowsky, G. (1978). On the number of prime implicants. **Discrete Mathematics**,
24**, 7–11.**
Darwiche, A. (1999). Compiling knowledge into decomposable negation normal form. In **Proceedings**
of International Joint Conference on Artificial Intelligence (IJCAI'99)**, pp. 284–289. Morgan**
Kaufmann, California.

Darwiche, A. (2001a). Decomposable negation normal form. Journal of the ACM, 48 **(4), 608–647.**
Darwiche, A. (2001b). On the tractability of counting theory models and its application to belief revision and truth maintenance. Journal of Applied Non-Classical Logics, 11 **(1-2), 11–34.**
Darwiche, A., & Huang, J. (2002). Testing equivalence probabilistically. Tech. rep. D–123, Computer Science Department, UCLA, Los Angeles, Ca 90095.

de Kleer, J. (1992). An improved incremental algorithm for generating prime implicates. In **Proc.**
of the 10th National Conference on Artificial Intelligence (AAAI'92)**, pp. 780–785, San Jose,**
California.

Dechter, R., & Rish, I. (1994). Directional resolution: the Davis-Putnam procedure, revisited. In Proceedings of the Fourth International Conference on Principles of Knowledge Representation and Reasoning (KR'94)**, pp. 134–145, Bonn.**
del Val, A. (1994). Tractable databases: How to make propositional unit resolution complete through compilation. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR'94)**, pp. 551–561. Morgan Kaufmann Publishers, Inc., San**
Mateo, California.