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 | Conference PDF | Archive PDF | Plain Text | 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 {elffers,giraldez,gocht,jakobn}@kth.se lsimon@labri.fr |
| 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. |