Bibliography

44 results

• [1] 2020
  A. Amarilli, F. Capelli, M. Monet, and P. Senellart, "Connecting Knowledge Compilation Classes and Width Parameters," Theory of Computing Systems, vol. 64, pp. 861–914, 2020. Amarilli_2020

  cSDD : ∨CcSDD : FOcSDD$_T$ : ∨CcSDD$_T$ : FOd-SDNNF : ∧BCd-SDNNF : ∨BCd-SDNNF : ∨Cd-SDNNF$_T$ : ∧Cd-SDNNF$_T$ : ∨Cdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨BCdec-DNNF : ∨Cdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF : ∨BCdec-SDNNF : ∨Cdec-SDNNF : FOdec-SDNNF$_T$ : ∧Cdec-SDNNF$_T$ : ∨CnFBDD : ¬CnFBDD : ∧BCnFBDD : ∧CnOBDD : ¬CnOBDD : ∧BCnOBDD : ∧CnOBDD : ∨BCnOBDD$_<$ : ¬CnOBDD$_<$ : ∧COBDD : ∨BCSDD : FOSDD$_T$ : ∧CSDD$_T$ : ∨CSDD$_T$ : FOSDNNF : ¬CSDNNF : ∧BCSDNNF : ∧CSDNNF : ∨BCSDNNF$_T$ : ¬CSDNNF$_T$ : ∧CTDD : ∨CTDD : FOTDD$_T$ : ∧CTDD$_T$ : ∨CTDD$_T$ : FOuFBDD : ∧BCuFBDD : ∧CuFBDD : ∨BCuOBDD : ∧BCuOBDD : ∧CuOBDD : ∨BCuOBDD : ∨CuOBDD$_<$ : ∧CuOBDD$_<$ : ∨Cd-SDNNF -> uOBDDd-SDNNF$_T$ -> d-SDNNFd-SDNNF$_T$ -> SDNNF$_T$d-SDNNF$_T$ -> uOBDD$_<$dec-DNNF -> d-DNNFdec-DNNF -> FBDDdec-SDNNF -> d-SDNNFdec-SDNNF -> dec-DNNFdec-SDNNF -> OBDDdec-SDNNF$_T$ -> d-SDNNF$_T$dec-SDNNF$_T$ -> dec-SDNNFdec-SDNNF$_T$ -> nFBDDdec-SDNNF$_T$ -> OBDD$_<$DNF -> d-SDNNFDNF -> nOBDD$_<$DNNF -> nFBDDFBDD -> dec-DNNFFBDD -> uFBDDnFBDD -> d-DNNFnFBDD -> DNNFnFBDD -> FBDDnOBDD -> nFBDDnOBDD -> SDNNFnOBDD$_<$ -> SDNNF$_T$OBDD -> dec-SDNNFOBDD -> uOBDDOBDD$_<$ -> dec-SDNNF$_T$OBDD$_<$ -> uOBDD$_<$SDNNF -> DNNFSDNNF -> nOBDDSDNNF$_T$ -> nOBDD$_<$uFBDD -> d-DNNFuFBDD -> FBDDuFBDD -> nFBDDuOBDD -> d-SDNNFuOBDD -> nOBDDuOBDD -> uFBDDuOBDD$_<$ -> d-SDNNF$_T$uOBDD$_<$ -> nOBDD$_<$

  cSDD : ∨CcSDD : FOcSDD$_T$ : ∨CcSDD$_T$ : FOd-SDNNF : ∧BCd-SDNNF : ∨BCd-SDNNF : ∨Cd-SDNNF$_T$ : ∧Cd-SDNNF$_T$ : ∨Cdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨BCdec-DNNF : ∨Cdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF : ∨BCdec-SDNNF : ∨Cdec-SDNNF : FOdec-SDNNF$_T$ : ∧Cdec-SDNNF$_T$ : ∨CnFBDD : ¬CnFBDD : ∧BCnFBDD : ∧CnOBDD : ¬CnOBDD : ∧BCnOBDD : ∧CnOBDD : ∨BCnOBDD$_<$ : ¬CnOBDD$_<$ : ∧COBDD : ∨BCSDD : FOSDD$_T$ : ∧CSDD$_T$ : ∨CSDD$_T$ : FOSDNNF : ¬CSDNNF : ∧BCSDNNF : ∧CSDNNF : ∨BCSDNNF$_T$ : ¬CSDNNF$_T$ : ∧CTDD : ∨CTDD : FOTDD$_T$ : ∧CTDD$_T$ : ∨CTDD$_T$ : FOuFBDD : ∧BCuFBDD : ∧CuFBDD : ∨BCuOBDD : ∧BCuOBDD : ∧CuOBDD : ∨BCuOBDD : ∨CuOBDD$_<$ : ∧CuOBDD$_<$ : ∨Cd-SDNNF -> uOBDDd-SDNNF$_T$ -> d-SDNNFd-SDNNF$_T$ -> SDNNF$_T$d-SDNNF$_T$ -> uOBDD$_<$dec-DNNF -> d-DNNFdec-DNNF -> FBDDdec-SDNNF -> d-SDNNFdec-SDNNF -> dec-DNNFdec-SDNNF -> OBDDdec-SDNNF$_T$ -> d-SDNNF$_T$dec-SDNNF$_T$ -> dec-SDNNFdec-SDNNF$_T$ -> nFBDDdec-SDNNF$_T$ -> OBDD$_<$DNF -> d-SDNNFDNF -> nOBDD$_<$DNNF -> nFBDDFBDD -> dec-DNNFFBDD -> uFBDDnFBDD -> d-DNNFnFBDD -> DNNFnFBDD -> FBDDnOBDD -> nFBDDnOBDD -> SDNNFnOBDD$_<$ -> SDNNF$_T$OBDD -> dec-SDNNFOBDD -> uOBDDOBDD$_<$ -> dec-SDNNF$_T$OBDD$_<$ -> uOBDD$_<$SDNNF -> DNNFSDNNF -> nOBDDSDNNF$_T$ -> nOBDD$_<$uFBDD -> d-DNNFuFBDD -> FBDDuFBDD -> nFBDDuOBDD -> d-SDNNFuOBDD -> nOBDDuOBDD -> uFBDDuOBDD$_<$ -> d-SDNNF$_T$uOBDD$_<$ -> nOBDD$_<$ +
  bib
• [2] 2013
  P. Beame, J. Li, S. Roy, and D. Suciu, "Lower Bounds for Exact Model Counting and Applications in Probabilistic Databases," Proceedings of the Twenty-Ninth Conference on Uncertainty in Artificial Intelligence (UAI 2013), pp. 52–61, 2013. Beame_2013
  bib
• [3] 2015
  Paul Beame and Vincent Liew, "New Limits for Knowledge Compilation and Applications to Exact Model Counting," Proceedings of the Thirty-First Conference on Uncertainty in Artificial Intelligence, UAI 2015, July 12-16, 2015, Amsterdam, The Netherlands, pp. 131–140, 2015. Beame_2015

  FBDD -> SDD

  FBDD -> SDD +
  bib
• [4] 1980
  M. Blum, A. K. Chandra, and M. N. Wegman, "Equivalence of free boolean graphs can be decided probabilistically in polynomial time," Information Processing Letters, vol. 10, pp. 80–82, 1980. Blum_1980

  FBDD : EQ

  FBDD : EQ +
  bib
• [5] 2019
  B. Bollig and M. Buttkus, "On the Relative Succinctness of Sentential Decision Diagrams," Theory of Computing Systems, vol. 63, pp. 1250–1277, 2019. Bollig_2019

  SDD$_T$ -> FBDD

  SDD$_T$ -> FBDD +
  bib
• [6] 2014
  S. Bova, F. Capelli, S. Mengel, and F. Slivovsky, "A Strongly Exponential Separation of DNNFs from CNF Formulas," 2014. Bova_2014

  cSDD : ∧CcSDD$_T$ : ∧Cd-SDNNF : ∧Cd-SDNNF$_T$ : ∧Cdec-DNNF : ∧Cdec-SDNNF : ∧Cdec-SDNNF$_T$ : ∧CDNF : ¬CDNF : ∧CDNNF : ¬CDNNF : ∧CnFBDD : ¬CnFBDD : ∧CnOBDD : ¬CnOBDD : ∧CnOBDD$_<$ : ¬CnOBDD$_<$ : ∧CSDD : ∧CSDD$_T$ : ∧CSDNNF : ¬CSDNNF : ∧CSDNNF$_T$ : ¬CSDNNF$_T$ : ∧CTDD : ∧CTDD$_T$ : ∧CuFBDD : ∧CuOBDD : ∧CuOBDD$_<$ : ∧CCNF -> DNNFDNNF -> d-DNNF

  cSDD : ∧CcSDD$_T$ : ∧Cd-SDNNF : ∧Cd-SDNNF$_T$ : ∧Cdec-DNNF : ∧Cdec-SDNNF : ∧Cdec-SDNNF$_T$ : ∧CDNF : ¬CDNF : ∧CDNNF : ¬CDNNF : ∧CnFBDD : ¬CnFBDD : ∧CnOBDD : ¬CnOBDD : ∧CnOBDD$_<$ : ¬CnOBDD$_<$ : ∧CSDD : ∧CSDD$_T$ : ∧CSDNNF : ¬CSDNNF : ∧CSDNNF$_T$ : ¬CSDNNF$_T$ : ∧CTDD : ∧CTDD$_T$ : ∧CuFBDD : ∧CuOBDD : ∧CuOBDD$_<$ : ∧CCNF -> DNNFDNNF -> d-DNNF +
  bib
• [7] 2016
  S. Bova, F. Capelli, S. Mengel, and F. Slivovsky, "Knowledge Compilation Meets Communication Complexity," Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016), pp. 1008–1014, 2016. Bova_2016

  d-DNNF : ∨BCdec-DNNF : ∨BCuFBDD : ∨BCDNNF -> d-DNNFPI -> DNNFuFBDD -> FBDD

  d-DNNF : ∨BCdec-DNNF : ∨BCuFBDD : ∨BCDNNF -> d-DNNFPI -> DNNFuFBDD -> FBDD +
  bib
• [8] 2016
  S. Bova, "SDDs Are Exponentially More Succinct than OBDDs," Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, pp. 929–935, 2016. Bova_2016_a

  cSDD -> OBDDcSDD$_T$ -> OBDDcSDD$_T$ -> OBDD$_<$

  cSDD -> OBDDcSDD$_T$ -> OBDDcSDD$_T$ -> OBDD$_<$ +
  bib
• [9] 1986
  R. E. Bryant, "Graph-based algorithms for boolean function manipulation," IEEE Transactions on Computers, vol. C-35, pp. 677–691, 1986. Bryant_1986

  OBDD : CTOBDD$_<$ : COOBDD$_<$ : CTOBDD$_<$ : EQOBDD$_<$ : MEOBDD$_<$ : VAOBDD$_<$ : ¬COBDD$_<$ : ∧BCOBDD$_<$ : ∨BCOBDD$_<$ : CD

  OBDD : CTOBDD$_<$ : COOBDD$_<$ : CTOBDD$_<$ : EQOBDD$_<$ : MEOBDD$_<$ : VAOBDD$_<$ : ¬COBDD$_<$ : ∧BCOBDD$_<$ : ∨BCOBDD$_<$ : CD +
  bib
• [10] 1991
  R. E. Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication," IEEE Transactions on Computers, vol. 40, pp. 205–213, 1991. Bryant_1991

  cSDD$_T$ -> OBDD$_<$FBDD -> OBDDuOBDD -> OBDD

  cSDD$_T$ -> OBDD$_<$FBDD -> OBDDuOBDD -> OBDD +
  bib
• [11] 1992
  R. E. Bryant, "Symbolic Boolean manipulation with ordered binary-decision diagrams," ACM Computing Surveys, vol. 24, pp. 293–318, 1992. Bryant_1992

  FBDD : COFBDD : CTFBDD : VAOBDD$_<$ : CTOBDD$_<$ : EQ

  FBDD : COFBDD : CTFBDD : VAOBDD$_<$ : CTOBDD$_<$ : EQ +
  bib
• [12] 2016
  Florent Capelli, "Structural Restrictions of CNF-formulas: Applications to Model Counting and Knowledge Compilation," 2016. Capelli_2016

  FBDD -> SDNNF

  FBDD -> SDNNF +
  bib
• [13] 2026
  F. Capelli, Y. Choi, S. Mengel, M. Muñoz, and G. Van den Broeck, "A Canonical Generalization of OBDD," 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026), vol. 377, pp. 10:1–10:19, 2026. Capelli_2026

  SDD$_T$ : FOTDD : ¬CTDD : ∧BCTDD : ∧CTDD : ∨BCTDD : ∨CTDD : CDTDD : FOTDD : SFOTDD$_T$ : ¬CTDD$_T$ : ∧BCTDD$_T$ : ∧CTDD$_T$ : ∨CTDD$_T$ : CDTDD$_T$ : FOOBDD -> TDDOBDD$_<$ -> TDD$_T$TDD -> d-SDNNFTDD -> SDDTDD$_T$ -> d-SDNNF$_T$TDD$_T$ -> OBDDTDD$_T$ -> SDD$_T$TDD$_T$ -> TDD

  SDD$_T$ : FOTDD : ¬CTDD : ∧BCTDD : ∧CTDD : ∨BCTDD : ∨CTDD : CDTDD : FOTDD : SFOTDD$_T$ : ¬CTDD$_T$ : ∧BCTDD$_T$ : ∧CTDD$_T$ : ∨CTDD$_T$ : CDTDD$_T$ : FOOBDD -> TDDOBDD$_<$ -> TDD$_T$TDD -> d-SDNNFTDD -> SDDTDD$_T$ -> d-SDNNF$_T$TDD$_T$ -> OBDDTDD$_T$ -> SDD$_T$TDD$_T$ -> TDD +
  bib
• [14] 1978
  A. K. Chandra and G. Markowsky, "On the Number of Prime Implicants," Discrete Mathematics, vol. 24, pp. 7–11, 1978. Chandra_1978

  IP : ∨BCIP : SFOPI : ∧BC

  IP : ∨BCIP : SFOPI : ∧BC +
  bib
• [15] 1971
  S. A. Cook, "The Complexity of Theorem-Proving Procedures," Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158, 1971. Cook_1971

  CNF : CO

  CNF : CO +
  bib
• [16] 2001
  A. Darwiche, "Decomposable Negation Normal Form," Journal of the ACM, vol. 48, pp. 608–647, 2001. Darwiche_2001a

  DNNF : CODNNF : FOMODS : FO

  DNNF : CODNNF : FOMODS : FO +
  bib
• [17] 2001
  A. Darwiche, "On the Tractable Counting of Theory Models and its Application to Truth Maintenance and Belief Revision," Journal of Applied Non-Classical Logics, vol. 11, pp. 11–34, 2001. Darwiche_2001b

  d-DNNF : CTcSDD : ∧BCcSDD : ∧CcSDD$_T$ : ∧Cd-DNNF : ∧BCd-SDNNF : ∧BCd-SDNNF : ∧Cd-SDNNF$_T$ : ∧Cdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨Cdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF$_T$ : ∧CDNNF : ∧BCFBDD : ∧BCOBDD : ∧BCSDD : ∧BCSDD : ∧CSDD$_T$ : ∧CTDD : ∧BCTDD : ∧CTDD$_T$ : ∧CuFBDD : ∧BCuFBDD : ∧CuOBDD : ∧BCuOBDD : ∧CuOBDD$_<$ : ∧Cd-DNNF -> DNNFd-DNNF -> FBDDd-SDNNF -> uOBDDd-SDNNF$_T$ -> uOBDD$_<$dec-DNNF -> FBDDdec-SDNNF -> OBDDdec-SDNNF$_T$ -> nFBDDdec-SDNNF$_T$ -> OBDD$_<$DNNF -> nFBDDSDNNF -> nOBDDSDNNF$_T$ -> nOBDD$_<$

  d-DNNF : CTcSDD : ∧BCcSDD : ∧CcSDD$_T$ : ∧Cd-DNNF : ∧BCd-SDNNF : ∧BCd-SDNNF : ∧Cd-SDNNF$_T$ : ∧Cdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨Cdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF$_T$ : ∧CDNNF : ∧BCFBDD : ∧BCOBDD : ∧BCSDD : ∧BCSDD : ∧CSDD$_T$ : ∧CTDD : ∧BCTDD : ∧CTDD$_T$ : ∧CuFBDD : ∧BCuFBDD : ∧CuOBDD : ∧BCuOBDD : ∧CuOBDD$_<$ : ∧Cd-DNNF -> DNNFd-DNNF -> FBDDd-SDNNF -> uOBDDd-SDNNF$_T$ -> uOBDD$_<$dec-DNNF -> FBDDdec-SDNNF -> OBDDdec-SDNNF$_T$ -> nFBDDdec-SDNNF$_T$ -> OBDD$_<$DNNF -> nFBDDSDNNF -> nOBDDSDNNF$_T$ -> nOBDD$_<$ +
  bib
• [18] 2002
  A. Darwiche and P. Marquis, "A Knowledge Compilation Map," Journal of Artificial Intelligence Research, vol. 17, pp. 229–264, 2002. Darwiche_2002

  CNF : IMCNF : VAd-DNNF : CTDNF : VADNNF : COIP : CTIP : IMIP : SEMODS : COMODS : CTOBDD : CTOBDD : EQOBDD : SEPI : CEPI : CTPI : SECNF : ∧CCNF : ∨BCCNF : ∨CCNF : CDCNF : FOcSDD : ∧CcSDD : ∨CcSDD$_T$ : ∨Cd-DNNF : ∧BCd-DNNF : ∨BCd-DNNF : CDd-SDNNF : ∧Cd-SDNNF : ∨Cd-SDNNF$_T$ : ∨Cdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨BCdec-DNNF : ∨Cdec-SDNNF : ∧Cdec-SDNNF : ∨Cdec-SDNNF$_T$ : ∨CDNF : ¬CDNF : ∧BCDNF : ∧CDNF : ∨CDNF : FODNNF : ¬CDNNF : ∧BCDNNF : ∧CDNNF : ∨CDNNF : CDDNNF : FOFBDD : ¬CFBDD : ∧BCFBDD : ∧CFBDD : ∨CFBDD : CDIP : ¬CIP : ∧BCIP : ∧CIP : ∨BCIP : CDIP : SFOMODS : ¬CMODS : ∧BCMODS : ∧CMODS : ∨BCMODS : FOnFBDD : ∧BCnFBDD : ∧CNNF : ¬CNNF : ∧CNNF : CDNNF : FOnOBDD : ∧COBDD : ¬COBDD : ∧BCOBDD : ∧COBDD : ∨COBDD : CDOBDD : SFOOBDD$_<$ : ∨CPI : ¬CPI : ∧BCPI : ∨BCPI : ∨CPI : CDPI : FOSDD : ∧CSDD$_T$ : ∨CSDNNF : ∧CTDD : ∧CTDD : ∨CTDD$_T$ : ∨CuFBDD : ∧BCuFBDD : ∧CuFBDD : ∨BCuOBDD : ∧CuOBDD : ∨CuOBDD$_<$ : ∨CCNF -> NNFCNF -> PId-DNNF -> MODSdec-SDNNF -> OBDDdec-SDNNF$_T$ -> OBDD$_<$DNF -> d-DNNFDNF -> DNNFDNF -> IPDNNF -> NNFFBDD -> d-DNNFIP -> CNFIP -> DNFIP -> FBDDIP -> MODSMODS -> CNFMODS -> d-DNNFMODS -> DNFMODS -> IPMODS -> OBDD$_<$OBDD -> FBDDOBDD$_<$ -> CNFOBDD$_<$ -> DNFPI -> CNFPI -> DNFPI -> FBDDPI -> MODS

  CNF : IMCNF : VAd-DNNF : CTDNF : VADNNF : COIP : CTIP : IMIP : SEMODS : COMODS : CTOBDD : CTOBDD : EQOBDD : SEPI : CEPI : CTPI : SECNF : ∧CCNF : ∨BCCNF : ∨CCNF : CDCNF : FOcSDD : ∧CcSDD : ∨CcSDD$_T$ : ∨Cd-DNNF : ∧BCd-DNNF : ∨BCd-DNNF : CDd-SDNNF : ∧Cd-SDNNF : ∨Cd-SDNNF$_T$ : ∨Cdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨BCdec-DNNF : ∨Cdec-SDNNF : ∧Cdec-SDNNF : ∨Cdec-SDNNF$_T$ : ∨CDNF : ¬CDNF : ∧BCDNF : ∧CDNF : ∨CDNF : FODNNF : ¬CDNNF : ∧BCDNNF : ∧CDNNF : ∨CDNNF : CDDNNF : FOFBDD : ¬CFBDD : ∧BCFBDD : ∧CFBDD : ∨CFBDD : CDIP : ¬CIP : ∧BCIP : ∧CIP : ∨BCIP : CDIP : SFOMODS : ¬CMODS : ∧BCMODS : ∧CMODS : ∨BCMODS : FOnFBDD : ∧BCnFBDD : ∧CNNF : ¬CNNF : ∧CNNF : CDNNF : FOnOBDD : ∧COBDD : ¬COBDD : ∧BCOBDD : ∧COBDD : ∨COBDD : CDOBDD : SFOOBDD$_<$ : ∨CPI : ¬CPI : ∧BCPI : ∨BCPI : ∨CPI : CDPI : FOSDD : ∧CSDD$_T$ : ∨CSDNNF : ∧CTDD : ∧CTDD : ∨CTDD$_T$ : ∨CuFBDD : ∧BCuFBDD : ∧CuFBDD : ∨BCuOBDD : ∧CuOBDD : ∨CuOBDD$_<$ : ∨CCNF -> NNFCNF -> PId-DNNF -> MODSdec-SDNNF -> OBDDdec-SDNNF$_T$ -> OBDD$_<$DNF -> d-DNNFDNF -> DNNFDNF -> IPDNNF -> NNFFBDD -> d-DNNFIP -> CNFIP -> DNFIP -> FBDDIP -> MODSMODS -> CNFMODS -> d-DNNFMODS -> DNFMODS -> IPMODS -> OBDD$_<$OBDD -> FBDDOBDD$_<$ -> CNFOBDD$_<$ -> DNFPI -> CNFPI -> DNFPI -> FBDDPI -> MODS +
  bib
• [19] 2011
  A. Darwiche, "SDD: A New Canonical Representation of Propositional Knowledge Bases," Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI 2011), pp. 819–826, 2011. Darwiche_2011

  cSDD$_T$ : ∧CcSDD$_T$ : ∨CcSDD$_T$ : FOSDD : ¬CSDD : CDSDD : SFOSDD$_T$ : ¬CSDD$_T$ : ∧BCSDD$_T$ : ∨BCSDD$_T$ : CDcSDD$_T$ -> cSDDOBDD$_<$ -> cSDD$_T$SDD$_T$ -> SDDuOBDD$_<$ -> SDD

  cSDD$_T$ : ∧CcSDD$_T$ : ∨CcSDD$_T$ : FOSDD : ¬CSDD : CDSDD : SFOSDD$_T$ : ¬CSDD$_T$ : ∧BCSDD$_T$ : ∨BCSDD$_T$ : CDcSDD$_T$ -> cSDDOBDD$_<$ -> cSDD$_T$SDD$_T$ -> SDDuOBDD$_<$ -> SDD +
  bib
• [20] 2002
  A. Darwiche and J. Huang, "Testing equivalence probabilistically," 2002. Darwiche_Huang_2002

  d-DNNF : EQ

  d-DNNF : EQ +
  bib
• [21] 2007
  J. Huang and A. Darwiche, "The Language of Search," Journal of Artificial Intelligence Research, vol. 29, pp. 191–219, 2007. darwiche2007language
  bib
• [22] 2013
  H. Fargier, P. Marquis, and A. Niveau, "Towards a knowledge compilation map for heterogeneous representation languages," Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, pp. 877–883, 2013. Fargier_2013
  bib
• [23] 1978
  S. Fortune, J. E. Hopcroft, and E. M. Schmidt, "The Complexity of Equivalence and Containment for Free Single Variable Program Schemes," Automata, Languages and Programming, vol. 62, pp. 227–240, 1978. Fortune_1978

  OBDD : EQ

  OBDD : EQ +
  bib
• [24] 1994
  J. Gergov and C. Meinel, "Efficient Boolean manipulation with OBDD's can be extended to FBDD's," IEEE Transactions on Computers, vol. 43, pp. 1197–1209, 1994. Gergov_1994

  FBDD : COFBDD : CTFBDD : VA

  FBDD : COFBDD : CTFBDD : VA +
  bib
• [25] 1995
  G. Gogic, H. Kautz, C. H. Papadimitriou, and B. Selman, "The Comparative Linguistics of Knowledge Representation," Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI-95), pp. 862–869, 1995. Gogic_1995
  bib
• [26] 2016
  N. S. Kaleyski, "Boolean Methods in Knowledge Compilation," 2016. Kaleyski_2016

  MODS -> PI

  MODS -> PI +
  bib
• [27] 2003
  J. Lang, P. Liberatore, and P. Marquis, "Propositional Independence: Formula-Variable Independence and Forgetting," Journal of Artificial Intelligence Research, vol. 18, pp. 391–443, 2003. Lang_2003

  DNF : FO

  DNF : FO +
  bib
• [28] 1973
  L. A. Levin, "Universal Search Problems," Problems of Information Transmission, vol. 9, pp. 265–266, 1973. Levin_1973

  CNF : CO

  CNF : CO +
  bib
• [29] 2000
  P. Marquis, "Consequence Finding Algorithms," Algorithms for Uncertainty and Defeasible Reasoning, vol. 5, pp. 41–145, 2000. Marquis_2000

  IP : ∧BCPI : ∨BCPI : CDPI : FO

  IP : ∧BCPI : ∨BCPI : CDPI : FO +
  bib
• [30] 1998
  C. Meinel and T. Theobald, "Algorithms and Data Structures in VLSI Design: OBDD–-Foundations and Applications," 1998. Meinel_Theobald_1998

  OBDD : EQOBDD : SEOBDD$_<$ : EQ

  OBDD : EQOBDD : SEOBDD$_<$ : EQ +
  bib
• [31] 2008
  K. Pipatsrisawat and A. Darwiche, "New Compilation Languages Based on Structured Decomposability," Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08), pp. 517–522, 2008. Pipatsrisawat_2008

  d-SDNNF : CDd-SDNNF : FOd-SDNNF$_T$ : ∧BCd-SDNNF$_T$ : CDSDNNF : CDSDNNF : FOSDNNF$_T$ : ¬CSDNNF$_T$ : ∧BCSDNNF$_T$ : ∧CSDNNF$_T$ : ∨CSDNNF$_T$ : CDSDNNF$_T$ : FOSDNNF$_T$ -> SDNNF

  d-SDNNF : CDd-SDNNF : FOd-SDNNF$_T$ : ∧BCd-SDNNF$_T$ : CDSDNNF : CDSDNNF : FOSDNNF$_T$ : ¬CSDNNF$_T$ : ∧BCSDNNF$_T$ : ∧CSDNNF$_T$ : ∨CSDNNF$_T$ : CDSDNNF$_T$ : FOSDNNF$_T$ -> SDNNF +
  bib
• [32] 2010
  T. Pipatsrisawat, "Reasoning with Propositional Knowledge: Frameworks for Boolean Satisfiability and Knowledge Compilation," 2010. Pipatsrisawat_2010

  FBDD -> SDNNF

  FBDD -> SDNNF +
  bib
• [33] 2010
  T. Pipatsrisawat and A. Darwiche, "A Lower Bound on the Size of Decomposable Negation Normal Form," Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, pp. 345–350, 2010. Pipatsrisawat_Darwiche_2010

  cSDD : ∧BCcSDD : ∧CcSDD : ∨BCcSDD$_T$ : ∧Cd-SDNNF : ∧BCd-SDNNF : ∧Cd-SDNNF : ∨BCd-SDNNF$_T$ : ∧Cdec-DNNF : ∨Cdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF : ∨BCdec-SDNNF$_T$ : ∧COBDD : ∨BCSDD : ∧BCSDD : ∧CSDD : ∨BCSDD$_T$ : ∧CSDNNF : ∧BCSDNNF : ∨BCTDD : ∧BCTDD : ∧CTDD : ∨BCTDD$_T$ : ∧CuOBDD : ∧BCuOBDD : ∧CuOBDD : ∨BCuOBDD$_<$ : ∧Cd-SDNNF -> d-DNNFd-SDNNF -> SDNNFd-SDNNF -> uOBDDd-SDNNF$_T$ -> uOBDD$_<$dec-DNNF -> FBDDdec-SDNNF -> OBDDdec-SDNNF$_T$ -> nFBDDdec-SDNNF$_T$ -> OBDD$_<$DNNF -> nFBDDSDNNF -> nOBDDSDNNF$_T$ -> nOBDD$_<$

  cSDD : ∧BCcSDD : ∧CcSDD : ∨BCcSDD$_T$ : ∧Cd-SDNNF : ∧BCd-SDNNF : ∧Cd-SDNNF : ∨BCd-SDNNF$_T$ : ∧Cdec-DNNF : ∨Cdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF : ∨BCdec-SDNNF$_T$ : ∧COBDD : ∨BCSDD : ∧BCSDD : ∧CSDD : ∨BCSDD$_T$ : ∧CSDNNF : ∧BCSDNNF : ∨BCTDD : ∧BCTDD : ∧CTDD : ∨BCTDD$_T$ : ∧CuOBDD : ∧BCuOBDD : ∧CuOBDD : ∨BCuOBDD$_<$ : ∧Cd-SDNNF -> d-DNNFd-SDNNF -> SDNNFd-SDNNF -> uOBDDd-SDNNF$_T$ -> uOBDD$_<$dec-DNNF -> FBDDdec-SDNNF -> OBDDdec-SDNNF$_T$ -> nFBDDdec-SDNNF$_T$ -> OBDD$_<$DNNF -> nFBDDSDNNF -> nOBDDSDNNF$_T$ -> nOBDD$_<$ +
  bib
• [34] 1952
  W. V. Quine, "The Problem of Simplifying Truth Functions," The American Mathematical Monthly, vol. 59, pp. 521–531, 1952. Quine_1952
  bib
• [35] 1996
  D. Roth, "On the Hardness of Approximate Reasoning," Artificial Intelligence, vol. 82, pp. 273–302, 1996. Roth_1996

  PI : CT

  PI : CT +
  bib
• [36] 2000
  P. Savick\'y and S. Žák, "A Read-Once Lower Bound and a $(1,+k)$-Hierarchy for Branching Programs," Theoretical Computer Science, vol. 238, pp. 347–362, 2000. Savicky_Zak_2000

  SDD$_T$ -> FBDDuOBDD -> FBDD

  SDD$_T$ -> FBDDuOBDD -> FBDD +
  bib
• [37] 1996
  B. Selman and H. Kautz, "Knowledge compilation and theory approximation," J. ACM, vol. 43, pp. 193–224, 1996. Selman_1996
  bib
• [38] 2010
  A. Shpilka and A. Yehudayoff, "Arithmetic circuits: A survey of recent results and open questions," Foundations and Trends in Theoretical Computer Science, vol. 5, pp. 207–388, 2010. shpilka2010arithmetic
  bib
• [39] 1995
  D. Sieling and I. Wegener, "Graph Driven BDDs–-A New Data Structure for Boolean Functions," Theoretical Computer Science, vol. 141, pp. 283–310, 1995. Sieling_Wegener_1995

  FBDD -> OBDD

  FBDD -> OBDD +
  bib
• [40] —
  Anonymous, "A Tractable Circuit Zoo," forthcoming. TCZ_Forthcoming

  cSDD : ∧BCcSDD : ∧CcSDD : ∨BCcSDD : ∨CcSDD : FOcSDD$_T$ : ∧CcSDD$_T$ : ∨CcSDD$_T$ : FOd-DNNF : ∧BCd-DNNF : ∨BCd-DNNF : SFOd-SDNNF : ∧BCd-SDNNF : ∧Cd-SDNNF : ∨BCd-SDNNF : ∨Cd-SDNNF$_T$ : ∧Cd-SDNNF$_T$ : ∨Cd-SDNNF$_T$ : SFOdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨BCdec-DNNF : ∨Cdec-DNNF : SFOdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF : ∨BCdec-SDNNF : ∨Cdec-SDNNF : FOdec-SDNNF$_T$ : ∧Cdec-SDNNF$_T$ : ∨Cdec-SDNNF$_T$ : SFODNF : ∧CDNNF : ∧BCDNNF : ∧CFBDD : ∧BCFBDD : ∧CFBDD : ∨CnFBDD : ∧BCnFBDD : ∧CnFBDD : ∨CnFBDD : FOnOBDD : ∧BCnOBDD : ∧CnOBDD : ∨BCnOBDD : FOnOBDD$_<$ : ∧CnOBDD$_<$ : ∨CnOBDD$_<$ : FOOBDD : ∧BCOBDD : ∧COBDD : ∨BCOBDD : ∨COBDD : FOOBDD$_<$ : ∨COBDD$_<$ : FOSDD : ∧BCSDD : ∧CSDD : ∨BCSDD : FOSDD$_T$ : ∧CSDD$_T$ : ∨CSDD$_T$ : FOSDNNF : ∧BCSDNNF : ∧CSDNNF : ∨BCSDNNF$_T$ : ∧CTDD : ∧BCTDD : ∧CTDD : ∨BCTDD : ∨CTDD : FOTDD$_T$ : ∧CTDD$_T$ : ∨CTDD$_T$ : FOuFBDD : ∧BCuFBDD : ∧CuFBDD : ∨BCuFBDD : SFOuOBDD : ∧BCuOBDD : ∧CuOBDD : ∨BCuOBDD : ∨CuOBDD$_<$ : ∧CuOBDD$_<$ : ∨CuOBDD$_<$ : SFOcSDD -> FBDDcSDD$_T$ -> FBDDdec-SDNNF$_T$ -> OBDD$_<$OBDD -> SDNNF$_T$OBDD$_<$ -> OBDD

  cSDD : ∧BCcSDD : ∧CcSDD : ∨BCcSDD : ∨CcSDD : FOcSDD$_T$ : ∧CcSDD$_T$ : ∨CcSDD$_T$ : FOd-DNNF : ∧BCd-DNNF : ∨BCd-DNNF : SFOd-SDNNF : ∧BCd-SDNNF : ∧Cd-SDNNF : ∨BCd-SDNNF : ∨Cd-SDNNF$_T$ : ∧Cd-SDNNF$_T$ : ∨Cd-SDNNF$_T$ : SFOdec-DNNF : ∧BCdec-DNNF : ∧Cdec-DNNF : ∨BCdec-DNNF : ∨Cdec-DNNF : SFOdec-SDNNF : ∧BCdec-SDNNF : ∧Cdec-SDNNF : ∨BCdec-SDNNF : ∨Cdec-SDNNF : FOdec-SDNNF$_T$ : ∧Cdec-SDNNF$_T$ : ∨Cdec-SDNNF$_T$ : SFODNF : ∧CDNNF : ∧BCDNNF : ∧CFBDD : ∧BCFBDD : ∧CFBDD : ∨CnFBDD : ∧BCnFBDD : ∧CnFBDD : ∨CnFBDD : FOnOBDD : ∧BCnOBDD : ∧CnOBDD : ∨BCnOBDD : FOnOBDD$_<$ : ∧CnOBDD$_<$ : ∨CnOBDD$_<$ : FOOBDD : ∧BCOBDD : ∧COBDD : ∨BCOBDD : ∨COBDD : FOOBDD$_<$ : ∨COBDD$_<$ : FOSDD : ∧BCSDD : ∧CSDD : ∨BCSDD : FOSDD$_T$ : ∧CSDD$_T$ : ∨CSDD$_T$ : FOSDNNF : ∧BCSDNNF : ∧CSDNNF : ∨BCSDNNF$_T$ : ∧CTDD : ∧BCTDD : ∧CTDD : ∨BCTDD : ∨CTDD : FOTDD$_T$ : ∧CTDD$_T$ : ∨CTDD$_T$ : FOuFBDD : ∧BCuFBDD : ∧CuFBDD : ∨BCuFBDD : SFOuOBDD : ∧BCuOBDD : ∧CuOBDD : ∨BCuOBDD : ∨CuOBDD$_<$ : ∧CuOBDD$_<$ : ∨CuOBDD$_<$ : SFOcSDD -> FBDDcSDD$_T$ -> FBDDdec-SDNNF$_T$ -> OBDD$_<$OBDD -> SDNNF$_T$OBDD$_<$ -> OBDD +
  bib
• [41] 2015
  G. Van den Broeck and A. Darwiche, "On the Role of Canonicity in Knowledge Compilation," Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, pp. 1641–1648, 2015. VanDenBroeck_2015

  cSDD : ¬CcSDD : ∧BCcSDD : ∧CcSDD : ∨BCcSDD : ∨CcSDD : FOcSDD$_T$ : ¬CcSDD$_T$ : ∧BCcSDD$_T$ : ∧CcSDD$_T$ : ∨CcSDD$_T$ : CDcSDD$_T$ : FOcSDD$_T$ : SFOSDD : ∧BCSDD : ∧CSDD : ∨BCSDD : FOSDD$_T$ : ∧CSDD$_T$ : ∨CSDD$_T$ : FOcSDD -> SDDcSDD$_T$ -> SDD$_T$SDD -> d-SDNNFSDD$_T$ -> cSDD$_T$SDD$_T$ -> d-SDNNF$_T$

  cSDD : ¬CcSDD : ∧BCcSDD : ∧CcSDD : ∨BCcSDD : ∨CcSDD : FOcSDD$_T$ : ¬CcSDD$_T$ : ∧BCcSDD$_T$ : ∧CcSDD$_T$ : ∨CcSDD$_T$ : CDcSDD$_T$ : FOcSDD$_T$ : SFOSDD : ∧BCSDD : ∧CSDD : ∨BCSDD : FOSDD$_T$ : ∧CSDD$_T$ : ∨CSDD$_T$ : FOcSDD -> SDDcSDD$_T$ -> SDD$_T$SDD -> d-SDNNFSDD$_T$ -> cSDD$_T$SDD$_T$ -> d-SDNNF$_T$ +
  bib
• [42] 2024
  H. Vinall-Smeeth, "Structured d-DNNF Is Not Closed under Negation," Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI 2024), pp. 3593–3601, 2024. Vinall-Smeeth_2024

  d-DNNF : SFOd-SDNNF : ¬Cd-SDNNF : SFOd-SDNNF$_T$ : ∨BCd-SDNNF$_T$ : SFOdec-DNNF : SFOdec-SDNNF$_T$ : SFOuFBDD : SFOuOBDD : ¬CuOBDD : SFOuOBDD$_<$ : ∨BCuOBDD$_<$ : SFOd-SDNNF -> SDDd-SDNNF$_T$ -> SDD$_T$uOBDD$_<$ -> SDD

  d-DNNF : SFOd-SDNNF : ¬Cd-SDNNF : SFOd-SDNNF$_T$ : ∨BCd-SDNNF$_T$ : SFOdec-DNNF : SFOdec-SDNNF$_T$ : SFOuFBDD : SFOuOBDD : ¬CuOBDD : SFOuOBDD$_<$ : ∨BCuOBDD$_<$ : SFOd-SDNNF -> SDDd-SDNNF$_T$ -> SDD$_T$uOBDD$_<$ -> SDD +
  bib
• [43] 1987
  I. Wegener, "The Complexity of Boolean Functions," 1987. Wegener_1987

  dec-DNNF : ∨CFBDD : ∧CFBDD : ∨COBDD : ∧CIP -> FBDDPI -> FBDD

  dec-DNNF : ∨CFBDD : ∧CFBDD : ∨COBDD : ∧CIP -> FBDDPI -> FBDD +
  bib
• [44] 2000
  I. Wegener, "Branching Programs and Binary Decision Diagrams: Theory and Applications," 2000. Wegener_2000

  dec-DNNF : CDdec-SDNNF : CDdec-SDNNF$_T$ : CDFBDD : ∨BCFBDD : SFOnFBDD : ¬CnFBDD : CDnOBDD : ¬CnOBDD : CDnOBDD$_<$ : ¬CnOBDD$_<$ : ∧BCnOBDD$_<$ : ∧CnOBDD$_<$ : CDOBDD : ∨COBDD : FOOBDD$_<$ : ∨COBDD$_<$ : FOSDNNF : ¬CuFBDD : CDuOBDD : CDuOBDD$_<$ : ∧BCuOBDD$_<$ : CDd-SDNNF$_T$ -> uOBDD$_<$DNF -> OBDDnOBDD$_<$ -> nOBDDOBDD -> OBDD$_<$OBDD$_<$ -> uOBDD$_<$SDNNF$_T$ -> nOBDD$_<$uFBDD -> FBDDuOBDD -> FBDDuOBDD$_<$ -> nOBDD$_<$uOBDD$_<$ -> uOBDD

  dec-DNNF : CDdec-SDNNF : CDdec-SDNNF$_T$ : CDFBDD : ∨BCFBDD : SFOnFBDD : ¬CnFBDD : CDnOBDD : ¬CnOBDD : CDnOBDD$_<$ : ¬CnOBDD$_<$ : ∧BCnOBDD$_<$ : ∧CnOBDD$_<$ : CDOBDD : ∨COBDD : FOOBDD$_<$ : ∨COBDD$_<$ : FOSDNNF : ¬CuFBDD : CDuOBDD : CDuOBDD$_<$ : ∧BCuOBDD$_<$ : CDd-SDNNF$_T$ -> uOBDD$_<$DNF -> OBDDnOBDD$_<$ -> nOBDDOBDD -> OBDD$_<$OBDD$_<$ -> uOBDD$_<$SDNNF$_T$ -> nOBDD$_<$uFBDD -> FBDDuOBDD -> FBDDuOBDD$_<$ -> nOBDD$_<$uOBDD$_<$ -> uOBDD +
  bib