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 [1].
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
Authors: Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, Laurent Simon
IJCAI 2018 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We report results from extensive experiments on a wide range of benchmarks. |
| Researcher Affiliation | Academia | 1 KTH Royal Institute of Technology 2 Universit e de Bordeaux EMAIL EMAIL |
| Pseudocode | No | No pseudocode or clearly labeled algorithm blocks are present in the paper. The methodology is described in prose. |
| Open Source Code | Yes | Our experimental data can be examined at www.csc.kth.se/ jakobn/CDCL-insights, where we have also collected benchmarks and solver source code. |
| Open Datasets | Yes | Our experimental data can be examined at www.csc.kth.se/ jakobn/CDCL-insights, where we have also collected benchmarks and solver source code. |
| Dataset Splits | No | No explicit training/validation/test dataset splits are provided. The paper discusses evaluating solver configurations on 'families of instances' and measures performance using PAR scores, but it does not define dataset splits for training or validation in the typical machine learning sense. |
| Hardware Specification | Yes | We have run our experiments on a cluster with 6 AMD Opteron 6238 (2.6 GHz) cores with 16 GB of memory, using a timeout of 5000 seconds. |
| Software Dependencies | No | The paper states 'we have built an instrumented CDCL solver on top of Glucose [Audemard and Simon, 2009]', but it does not specify a version number for Glucose or any other software dependencies. It also mentions Mini Sat without a version. |
| Experiment Setup | Yes | To run our experiments we have built an instrumented CDCL solver on top of Glucose... where we have added a rich selection of extra options to analyse the interactions between (1) restart policy, (2) branching, (3) clause database management, and (4) clause learning... We have selected a generous subset of more than 650 different solver configurations, which still makes it possible to study how most settings interact. |