Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Accelerating SAT Solving by Common Subclause Elimination
Authors: Yaowei Yan, Chris Gutierrez, Jeriah Jn-Charles, Forrest Bao, Yuanlin Zhang
AAAI 2015 | Venue PDF | 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.' |