On CNF Conversion for SAT and SMT Enumeration: Benchmarks, Results and Plots

Experimental results for the paper:On CNF encoding for SAT and SMT enumeration, Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani. ArXiv, 2024.

Content:

aig-bench.zip iscas85-bench.zip syn-bool-bench.zip contain the inputs and results for the Boolean benchmarks. Each zip contains:

data/ that contains the input data

results-/ for each tested tool.

syn-lra-bench.zip wmi-bench.zip contain the inputs and results for the Boolean benchmarks. Each zip contains:

data/ that contains the input data

results-/ for each tested tool.

plot-d4, plot-msat, plot-tabularallsat, plot-tabularallsmt contain the plots for enumeration with different tools. 

plot-msat-sat contains the plot for plain satisfiability using MathSAT.

Results are stored in JSON files, where the field "mode" indicates the CNF transformation used to preprocess the input:

LAB for Tseitin CNF

LABELNEG_POL for Plaisted&Greenbaum CNF, using negative labels for subformulas occurring negatively only.

NNF_MUTEX_POL for NNF+Plaisted&Greenbaum CNF+mutex clauses, as described in the paper

The source code used to run the experiments is available at https://doi.org/10.5281/zenodo.14033422.