An Extended MaxSAT Preprocessor
MaxPre is developed by the Constraint Reasoning and Optimization Group at the Department of Computer Science, University of Helsinki, and implemented by Tuukka Korhonen.
MaxPre is an open-source (MIT licensed) preprocessor for weighted partial maximum satisfiability (MaxSAT). MaxPre implements a range of well-known and recent SAT-based preprocessing techniques as well as MaxSAT-specific techniques that make use of weights of soft clauses. Furthermore, MaxPre offers solution reconstruction, cardinality constraint encoding, and an API for integration into SAT-based MaxSAT solvers with minimal I/O overhead. More details can be found in  as well as in the github repository.
UsageAfter compilation, MaxPre can be run from the terminal using the command:
./maxpre <inputfile> <MODE> [options]Where <MODE> is either preprocess, reconstruct or solve:
ExamplesConsider the pipeline for first preprocessing a MaxSAT instance "test.wcnf", then solving the preprocessed instance using an external solver "mssolver" before reconstructing an optimal solution to "test.wcnf" from the optimal solution to the preprocessed instance. This can be done using the following three commands:
./maxpre test.wcnf preprocess -mapfile=test.map > preprocessed.wcnf ./mssolver < preprocessed.wcnf > sol0.sol ./maxpre sol0.sol reconstruct -mapfile=test.map > solution.solThe first command preprocesses "test.wcnf", outputting the preprocessed instance to the file "preprocessed.wcnf" and the reconstruction stack to the file "test.map". The second command invokes mssolver on the preprocessed instance, outputting an optimal model to the preprocessed instance to the file "sol0.sol". Finally, the third command reconstructs an optimal model to "test.wcnf" using an optimal model of "preprocessed.wcnf" and the reconstruction stack contained in the file "test.map". Alternatively, the single command
./maxpre test.wcnf solve -solver=./solver > solution.solcan be used in order to achieve the same effect.
Input formatMaxPre follows the standard formats used in the MaxSAT evaluation.. Going further, MaxPre also allows for easy specification of cardinality constraints. For example, a line of form
CARD l_1 l_2 ... l_n <= kin the input wcnf file is rewritten by MaxPre into hard clauses enforcing that at most k of the literals in the set l_1, ... , l_n can be set to true. Several other variations of cardinality constraints are supported, see the reference for more information.
The source code for MaxPre is available via github..
 MaxPre: An Extended MaxSAT Preprocessor.