Abstract:
UWrMaxSat is a quite new solver for MaxSAT and pseudo-Boolean problems. It has been created at the University of Wroclaw and can be characterized as a complete solver for...View moreMetadata
Abstract:
UWrMaxSat is a quite new solver for MaxSAT and pseudo-Boolean problems. It has been created at the University of Wroclaw and can be characterized as a complete solver for partial weighted MaxSAT instances, and, independently, for linear pseudo-Boolean optimizing and decision ones. The solver incrementally uses COMiniSatPS by Chanseok Oh (2016) as an underlying SAT solver, but may be compiled with other MiniSat-like solvers as well. It was developed on the top of our PB solver (called KP-MiniSat+) that was presented at Pragmatics of SAT 2018 and which is an extension of the well-known MiniSat+ solver. In its main configuration, UWrMaxSat applies a core-guided OLL procedure and uses the KP-MiniSat+ sorter-based pseudo-Boolean constraint encoding to translate cardinality constraints into CNF. The solver participated in MaxSAT Evaluation 2019, where it ranked second places in both main tracks (weighted and unweighted). The novel techniques applied in the solver are as follows: (1) a new encoding of cardinality and pseudo-Boolean constraints by 4-Way Merge Selection Networks, (2) a fast search algorithm for mixed-radix bases needed in the encoding, and (3) a combination of selected other optimization heuristics for weighted instances. Moreover, MaxPre preprocessor has been recently integrated with the solver.
Date of Conference: 09-11 November 2020
Date Added to IEEE Xplore: 24 December 2020
ISBN Information: