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

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