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

<p>Experimental results for the paper:<br><br><a title="Arxiv Link" href="https://arxiv.org/abs/2303.14971" target="_blank" rel="noopener">On CNF encoding for SAT and SMT enumeration</a>, Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani. ArXiv, 2024.</p> <p>Content:</p> <ul> <li><code>aig-bench.zip</code> <code>iscas85-bench.zip</code> <code>syn-bool-bench.zip</code> contain the inputs and results for the Boolean benchmarks. Each zip contains: <ul> <li><code>data/</code> that contains the input data</li> <li><code>results-&lt;tool&gt;/</code> for each tested tool.</li> </ul> </li> <li><code>syn-lra-bench.zip</code> <code>wmi-bench.zip</code> contain the inputs and results for the Boolean benchmarks. Each zip contains: <ul> <li><code>data/</code> that contains the input data</li> <li><code>results-&lt;tool&gt;/</code> for each tested tool.</li> </ul> </li> <li><code>plot-d4</code>,&nbsp;<code>plot-msat</code>,&nbsp;<code>plot-tabularallsat</code>,&nbsp;<code>plot-tabularallsmt</code> contain the plots for enumeration with different tools.&nbsp;</li> <li><code>plot-msat-sat</code> contains the plot for plain satisfiability using MathSAT.</li> </ul> <p>Results are stored in JSON files, where the field <code>"mode"</code> indicates the CNF transformation used to preprocess the input:</p> <ul> <li><code>LAB</code> for Tseitin CNF</li> <li><code>LABELNEG_POL</code> for Plaisted&amp;Greenbaum CNF, using negative labels for subformulas occurring negatively only.</li> <li><code>NNF_MUTEX_POL</code> for NNF+Plaisted&amp;Greenbaum CNF+mutex clauses, as described in the paper</li> </ul> <p>The source code used to run the experiments is available at&nbsp;<a href="https://doi.org/10.5281/zenodo.14033422" target="_blank" rel="noopener">https://doi.org/10.5281/zenodo.14033422</a>.</p> <p>&nbsp;</p>