Knowledge Compilation Meets Logical Separability
Authors: Junming Qiu, Wenqing Li, Zhanhao Xiao, Quanlong Guan, Liangda Fang, Zhao-Rong Lai, Qian Dong5851-5860
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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. ... The paper contains numerous theorems and propositions, such as Theorem 2 (Proof by induction), Theorem 3, Theorem 5 (Proof by induction), Theorem 8 (Proof by induction), and Proposition 1-12, all of which are theoretical contributions. |
| Researcher Affiliation | Academia | 1 Jinan University, Guangzhou 510632, China 2 Guangdong Institute of Smart Education, Guangzhou 510632, China 3 Sun Yat-sen University, Guangzhou 510006, China 4 Pazhou Lab, Guangzhou 510330, China 5 Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin 541004, China {2040697476jnu, eskii0706}@stu2020.jnu.edu.cn; xiaozhh9@mail.sysu.edu.cn; {gql, fangld, laizhr, dongq8}@jnu.edu.cn |
| Pseudocode | Yes | Definition 2. The procedure CO(α) is recursively defined as: CO( ) = 1, CO( ) = 0 and CO(l) = 1 CO(β1 βn) = min 1 i n{CO(βi)} CO(β1 βn) = max 1 i n{CO(βi)} ... Definition 5. ... Definition 9. ... (These definitions describe algorithms with clear, structured steps, resembling pseudocode even if not explicitly labeled as such). |
| Open Source Code | No | The paper does not contain any statement about releasing source code or provide a link to a code repository for the described methodology. The 'Acknowledgments' section mentions funding but no code. |
| Open Datasets | No | This paper is theoretical and focuses on logical properties and procedures. It does not involve empirical evaluation on datasets, thus no training data is mentioned. |
| Dataset Splits | No | This paper is theoretical and does not involve empirical evaluation or data splits for training, validation, or testing. |
| Hardware Specification | No | This is a theoretical paper and does not mention any specific hardware used for computational experiments. |
| Software Dependencies | No | This is a theoretical paper. It defines logical procedures and normal forms but does not specify any software dependencies with version numbers that would be required to reproduce an implementation. |
| Experiment Setup | No | This paper is theoretical and does not describe an experimental setup, hyperparameters, or training configurations, as it does not involve empirical evaluations. |