Using Resolution Proofs to Analyse CDCL SAT solvers

DOI10.5281/zenodo.3951538Zenodo3951538MaRDI QIDQ6700388FDOQ6700388

Dataset published at Zenodo repository.

Publication date: 19 July 2020

Copyright license: Creative Commons Attribution 4.0 International

Data for the article Janne I. Kokkala, Jakob Nordstrm: 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.

This page was built for dataset: Using Resolution Proofs to Analyse CDCL SAT solvers