Lifting (D)QBF Preprocessing and Solving Techniques to (D)SSAT
Authors: Che Cheng, Jie-Hong R. Jiang
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show that solving DSSAT via dependency elimination is highly applicable and that existing SSAT solvers may benefit from preprocessing. |
| Researcher Affiliation | Academia | 1Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan 2Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | Our implementation of the dependency elimination and preprocessing procedures, named DSSATpre,4 is written in C++ under the framework of HQSpre (Wimmer, Scholl, and Becker 2019). 4Available at https://github.com/NTU-ALCom Lab/DSSATpre. |
| Open Datasets | Yes | we conduct the experiment by taking DQBF benchmarks encoding partial equivalence checking (PEC) problem from (Fr ohlich et al. 2014) and (Scholl and Becker 2001)... The benchmarks are taken from https://github.com/jurajsic/DQBFbenchmarks. and We took the benchmarks of (Chen, Huang, and Jiang 2021) for evaluation... The benchmarks are taken from https://github.com/NTUALCom Lab/Clau SSat. |
| Dataset Splits | No | The paper uses established benchmark sets for evaluation but does not specify explicit training, validation, or test dataset splits within its experimental setup. |
| Hardware Specification | Yes | The experiments were conducted on a Linux machine with Intel Xeon Silver 4210 CPU processor at 2.2 GHz. |
| Software Dependencies | No | The paper mentions C++ as the implementation language and names several SSAT solvers (DC-SSAT, Clau SSat, Elim SSAT) that were used, but it does not specify version numbers for any software components. |
| Experiment Setup | Yes | All instances are subject to a time limit of 1000 seconds. The performance is judged based on the number of instances solved within the time limit and the penalized average runtime (PAR2) score, which penalizes unsolved instances with two times the time limit. |