Knowledge Compilation for Incremental and Checkable Stochastic Boolean Satisfiability
Authors: Che Cheng, Yun-Rong Luo, Jie-Hong R. Jiang
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show the benefits of the proposed knowledge compilation approach for SSAT in sharing computation efforts for multiple queries and producing checkable dec-DNNF logs with negligible overhead. Sharp SSAT is able to generate dec-DNNF proofs for all solvable instances, and cert-SSAT successfully turns 80.5 % of them into clausal proofs and verifies the clausal proofs within a reasonable time. |
| Researcher Affiliation | Academia | 1Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan 2University of Michigan, Ann Arbor MI, USA 3Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan r11943097@ntu.edu.tw, yunrong@umich.edu, jhjiang@ntu.edu.tw |
| Pseudocode | Yes | Algorithm 1 SSAT Evaluation with dec-DNNF |
| Open Source Code | Yes | Available at https://github.com/NTU-ALCom Lab/Sharp SSAT. Available at https://github.com/NTU-ALCom Lab/cert-SSAT. |
| Open Datasets | Yes | The benchmark formulas are taken from [Chen et al., 2021]. Available at https://github.com/NTU-ALCom Lab/Clau SSat. |
| Dataset Splits | No | The paper mentions generating random instances and various benchmark instances, but does not provide specific details on how the datasets were split for training, validation, or testing, nor does it refer to standard splits for these benchmarks. |
| Hardware Specification | Yes | The experiments were conducted on a Linux machine with an Intel Xeon Silver 4210 CPU processor at 2.2 GHz. We ran cert-SSAT on a Linux machine with a 12th Gen Intel Core i9-12900 processor |
| Software Dependencies | No | The paper mentions implementing Eval SSAT in C++ and modifying CPOG, but does not provide specific version numbers for these or any other software dependencies like compilers, libraries, or operating systems. |
| Experiment Setup | Yes | For the settings KC-p and KC-np, we set a time limit of 1000 sec for compilation and 100 sec for each query. If the compilation failed within the time limit, we view the queries as failed as well. For the setting baseline, we set a time limit of 200 sec for each query. We set a time limit of 1000 sec for Sharp SSAT and Eval SSAT and a time limit of 2500 sec for cpog-gen and cpog-check. |