## MaxPre## An Extended MaxSAT PreprocessorMaxPre is developed by the Constraint Reasoning and Optimization Group at the Department of Computer Science, University of Helsinki, and implemented by Tuukka Korhonen. ## AboutMaxPre 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 [1] 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: - If <MODE> = preprocess, then <inputfile> should be a file containing a MaxSAT instance in the standard (extended) DIMACS format, possibly containing additional cardinality constraints (see below). MaxPre then preprocesses the instance and outputs the preprocessed instance to the standard output. The flag "-mapfile=<MF>" can be used to specify the file (MF) to which the reconstruction stack (required for converting an optimal model of the preprocessed instance to an optimal model of the original instance) should be written.
- If <MODE> = reconstruct, then <inputfile> should be a file containing an optimal solution to the preprocessed MaxSAT instance. In this mode, the "-mapfile" flag is also required and should be a file containing the reconstruction stack produced by MaxPre when creating the preprocessed instance.
- If <MODE> = solve then <inputfile> should be a file containing a MaxSAT instance and the flag "-solver=./<mssolver>" should be used to specify an external MaxSAT solver binary. MaxPre then first preprocesses the input MaxSAT instance, then invokes <mssolver> on the preprocessed instance before reconstructing an optimal solution to the input instance from the output of <mssolver>
## 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 formCARD 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. ## AvailailityThe source code for MaxPre is available via github.. ## References
[1] |