TY - GEN
T1 - Knowledge Compilation Meets Logical Separability (CCF A)
AU - Qiu, Junming
AU - Li, Wenqing
AU - Xiao, Zhanhao
AU - Guan, Quanlong
AU - Fang, Liangda
AU - Lai, Zhao Rong
AU - Dong, Qian
N1 - Funding Information:
This paper was supported by the National Natural Science Foundation of China (Nos. 62077028, 61877029, 61906216, 62176103 and 61603152), the Guangdong Basic and Applied Basic Research Foundation (Nos. 2021A1515011873, 2021B0101420003, 2021B1515120048, 2020A1515010642, 2020B0909030005, 2020B1212030003, 2020ZDZX3013, 2019A050510024, 2019B1515120010 and 2018A030310633), the Specially Creative University Project of Guangdong (Nos. 2019KTSCX010 and 2018KTSCX016), the Fundamental Research Funds for the Central Universities (Nos. 11621418 and 21617349), the Science and Technology Project of Guangzhou (Nos. 202102080307, 202102021173 and 201902010041), and the Project of Guangxi Key Laboratory of Trusted Software (No. kx201604).
Publisher Copyright:
© 2022, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
PY - 2022/6/30
Y1 - 2022/6/30
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85147545542&partnerID=8YFLogxK
M3 - Conference Proceeding
AN - SCOPUS:85147545542
T3 - Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022
SP - 5851
EP - 5860
BT - AAAI-22 Technical Tracks 5
PB - Association for the Advancement of Artificial Intelligence
T2 - 36th AAAI Conference on Artificial Intelligence, AAAI 2022
Y2 - 22 February 2022 through 1 March 2022
ER -