MaxPre

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.

About

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 [1] as well as in the github repository.

Usage

After 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>
MaxPre also accepts a number of command line options. The flags can be used amongst other things to control the preprocessing techniques that are used and to impose time limits on the preprocessing. For more information, please see the README file in the repository or the reference.

Examples

Consider 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.sol
The 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.sol
can be used in order to achieve the same effect.

Input format

MaxPre 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 <= k
in 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.

Availaility

The source code for MaxPre is available via github..

References

[1] MaxPre: An Extended MaxSAT Preprocessor.
Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo.
In Serge Gaspers and Toby Walsh, editors, Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017), volume ????? of Lecture Notes in Computer Science, pages ???-???. Springer, 2017.
[doi:???] [pdf] [abstract/bibtex]