Experimental Repository for "Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability"

<h2>Experimental repository for "Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability".</h2> <h3>The directory is structured as follows:</h3> <ul> <li><code>data</code>: Data that has been processed into CSVs and the scripts to analyse the experiments.</li> <li><code>plots</code>: The plots generated from the data that are used in the paper.</li> <li><code>raw_data</code>: The raw data logs for the experiments and scripts to extract relevant data from the logs.</li> <li><code>source_code</code>: Source code for the checker <code>VeriPB</code> and the MaxSAT solver Pacose in the different variants used for the experiments. The Pacose version in <code>PacoseMaxSATSolver-baseline</code> is Pacose without proof logging, the version in <code>PacoseMaxSATSolver-certified</code> is Pacose with proof logging. Proof logging using only assumptions for the coarse convergence can be enabled via the option <code>--WithAssumptions</code>.</li> </ul> <h3>Install Requirements</h3> <p>To install and run the MaxSAT solver Pacose and the pseudo-Boolean proof checker VeriPB your need to have the following components installed:</p> <ul> <li>Python 3.6.9 or higher with pip and setuptools installed</li> <li>g++ 7.5.0 or higher</li> <li>libgmp</li> </ul> <p>These can be installed in Ubuntu / Debian via</p> <pre><code>sudo apt-get update &amp;&amp; apt-get install \ python3 \ python3-pip \ python3-dev \ g++ \ libgmp-dev pip3 install --user \ setuptools</code></pre> <h3>How to Run?</h3> <p>The MaxSAT solver Pacose can be compiled using the install script in <code>PacoseMaxSATSolver-certified</code>:</p> <p><code>./install</code></p> <p>To run Pacose with proof logging, where the proof should be written to <code>proof.pbp</code>, run the following command in the <code>PacoseMaxSATSolver-certified</code> directory:</p> <p><code>./bin/Pacose --proofFile proof.pbp instance.wcnf</code></p> <p>The proof can be checked with VeriPB. To compile VeriPB run the following in the <code>VeriPB</code> directory:</p> <p><code>pip install .</code></p> <p>To check the proof with VeriPB, run the following inside the <code>PacoseMaxSATSolver-certified</code> directory:</p> <p><code>veripb --wcnf instance.wcnf proof.pbp</code></p>