Accelerating SAT Solving by Common Subclause Elimination
Authors: Yaowei Yan, Chris Gutierrez, Jeriah Jn-Charles, Forrest Bao, Yuanlin Zhang
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Empirical study shows that CSE can significantly speed up SAT solving. |
| Researcher Affiliation | Academia | 1 Dept. of Electrical & Computer Engineering, University of Akron, Akron, OH, USA 2 Dept. of Computer Science, Texas Tech University, Lubbock, TX, USA |
| Pseudocode | No | The paper describes the algorithms in natural language and with examples but does not provide structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper mentions 'Additional info of this work will be posted at https://sites.google.com/site/yanyaw00/aaai15' which is a general information site and not a specific code repository or an explicit statement of code release. |
| Open Datasets | No | The paper states 'Two benchmarks from SAT competitions were used: SAT13: SAT Competition 2013, 3SAT: Problems that were explicitly labeled as 3SAT in SAT Competitions from 2007 to 2013' but does not provide specific links, DOIs, repositories, or formal citations for accessing these datasets. |
| Dataset Splits | No | The paper uses benchmarks from SAT competitions but does not provide specific details on training, validation, or test dataset splits. |
| Hardware Specification | No | The paper does not provide any specific hardware details such as GPU/CPU models, memory, or specific computing environments used for running experiments. |
| Software Dependencies | No | The paper does not list specific software dependencies with version numbers, such as programming languages, libraries, or solvers used for the experiments. |
| Experiment Setup | Yes | The paper describes experimental settings such as 'timeout 15m' and '48h', and parameters for the Frequency-based approach as 'Freq(s, f): Frequency-based approach with size threshold s and frequency threshold f. Only common subclauses containing more than s literals and appearing in more than f clauses will be replaced.' |