Data for the article Janne I. Kokkala, Jakob Nordström: Using Resolution Proofs to Analyse CDCL SAT solvers, accepted to the 26th International Conference on Principles and Practice of Constraint Programming. Files: solver.tgz – Source code of the modified Glucose 3.0 used in the experiments instances.tar – All CNF instances used in the experiments (compressed individually using xz). Note that these are the formulas obtained after preprocessing, so they are not the same as used in the SAT races and competitions they are obtained from. data-instances.txt – List of all benchmark instance filenames and IDs used to refer to them in other data files. data-solvers.txt – Parameters used for each solver configuration (see the paper for explanation of where they were used). data-solverstats.txt – For each solver configuration and instance, some data of the run data-proofsizes.txt – For each solver configuration and instance, sizes of untrimmed proof, the trimmed solver proof, and the proof output by DRAT-trim, measured both in number of learnt clauses and in number of clause usages – note that for the clause usage counts, all unit clauses are considered to be used only once at the end (since that would result to a shorter resolution proof and is more related to the solver performance) data-features.txt – For the solver used in the clause feature experiments, this file contains for each instance the frequency distribution of each feature (both absolute and percentile rank) plots-features.pdf – Larger versions of the feature plots in the paper, including plots not shown in the paper. plots-proofsizes.pdf – Plots of the data for the pairwise solver proof size comparison experiments.

The computational experiments used resources provided by the Swedish National Infrastructure for Computing (SNIC) at the High Performance Computing Center North (HPC2N) at Umeå University. The authors were supported by the Swedish Research Council grant 2016-00782, and the second author also received funding from the Independent Research Fund Denmark (DFF) grant 9040-00389B.