Knowledge Compilation Meets Logical Separability (CCF A)

Junming Qiu, Wenqing Li, Zhanhao Xiao, Quanlong Guan*, Liangda Fang*, Zhao Rong Lai, Qian Dong

*Corresponding author for this work

Research output: Chapter in Book or Report/Conference proceedingConference Proceedingpeer-review

1 Citation (Scopus)


Knowledge compilation is an alternative solution to address demanding reasoning tasks with high complexity via converting knowledge bases into a suitable target language. Interestingly, the notion of logical separability, proposed by Levesque, offers a general explanation for the tractability of clausal entailment for two remarkable languages: decomposable negation normal form and prime implicates. It is interesting to explore what role logical separability on earth plays in problem tractability. In this paper, we apply the notion of logical separability in three reasoning problems within the context of propositional logic: satisfiability check (CO), clausal entailment check (CE) and model counting (CT), contributing to three corresponding polytime procedures. We provide three logical separability based properties: CO-logical separability, CE-logical separability and CT-logical separability. We then identify three novel normal forms: CO-LSNNF, CE-LSNNF and CT-LSNNF based on the above properties. Besides, we show that every normal form is the necessary and sufficient condition under which the corresponding procedure is correct. We finally integrate the above four normal forms into the knowledge compilation map.

Original languageEnglish
Title of host publicationAAAI-22 Technical Tracks 5
PublisherAssociation for the Advancement of Artificial Intelligence
Number of pages10
ISBN (Electronic)1577358767, 9781577358763
Publication statusPublished - 30 Jun 2022
Externally publishedYes
Event36th AAAI Conference on Artificial Intelligence, AAAI 2022 - Virtual, Online
Duration: 22 Feb 20221 Mar 2022

Publication series

NameProceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022


Conference36th AAAI Conference on Artificial Intelligence, AAAI 2022
CityVirtual, Online


Dive into the research topics of 'Knowledge Compilation Meets Logical Separability (CCF A)'. Together they form a unique fingerprint.

Cite this