On Pre- and Inprocessing for Weighted MaxSAT
Modern competitive solvers employ various pre- and inprocessing techniques to efficiently tackle complex problems. This work introduces two pre- and inprocessing techniques to improve solving weighted partial MaxSAT problems: Generalized Boolean Multilevel Optimization (GBMO) and Trimming MaxSAT (TrimMaxSAT).
GBMO refines and extends Boolean Multilevel Optimization (BMO), thereby splitting instances due to their distribution of weights into multiple less complex subproblems, which are solved one after the other to obtain the overall solution.
The second technique, TrimMaxSAT, finds unsatisfiable soft clauses and removes them from the instance. This reduces the complexity of the MaxSAT instance and works especially well in combination with GBMO. The proposed algorithm works incrementally in a binary search fashion, testing the satisfiability of every soft clause. Furthermore, as a by-product, typically an initial weight close to the maximum is found, which is in turn advantageous w.r.t. the size of e.g. the Dynamic Polynomial Watchdog (DPW) encoding.
Experimental results show the effectiveness of both techniques on a large set of benchmarks from a hardware security application and from the 2019 MaxSAT Evaluation. In particular for the hardest of the application benchmarks, the solver Pacose with GBMO and TrimMaxSAT performs best compared to the MaxSAT Evaluation solvers of 2019. For the benchmarks of the 2019 MaxSAT Evaluation, we show that with the proposed techniques the top solver combination solves significantly more instances.
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:30
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. Summers University of British Columbia
|Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories|
Martin Bromberger MPI-INF, Alberto Fiori Max Planck Institute for Informatics, Christoph Weidenbach MPI-INFMedia Attached
|Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching|
Jochen Hoenicke University of Freiburg, Tanja Schindler University of FreiburgMedia Attached
|On Pre- and Inprocessing for Weighted MaxSAT|
Tobias Paxian University of Freiburg, Pascal Raiola University of Freiburg, Bernd Becker Albert-Ludwigs-University FreiburgMedia Attached
|Compositional Satisfiability Solving in Separation Logic|
Quang Loc Le University College London, UKMedia Attached