Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 19:00 - 19:15 at VMCAI - Decision Procedures Chair(s): Alexander J. Summers

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30: Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. SummersUniversity of British Columbia
18:30 - 18:45
Talk
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Martin BrombergerMPI-INF, Alberto FioriMax Planck Institute for Informatics, Christoph WeidenbachMPI-INF
Media Attached
18:45 - 19:00
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen HoenickeUniversity of Freiburg, Tanja SchindlerUniversity of Freiburg
Media Attached
19:00 - 19:15
Talk
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Tobias PaxianUniversity of Freiburg, Pascal RaiolaUniversity of Freiburg, Bernd BeckerAlbert-Ludwigs-University Freiburg
Media Attached
19:15 - 19:30
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc LeUniversity College London, UK
Media Attached