资源Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT Jeremias Berg and Paul Saikko and Matti Ja?rvisalo

Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT Jeremias Berg and Paul Saikko and Matti Ja?rvisalo

2019-11-18 | |  34 |   1 |   0
Abstract Solvers for the Maximum satisfiability (MaxSAT) problem find an increasing number of applications today. We focus on improving MaxHS—one of the most successful recent MaxSAT algorithms— via SAT-based preprocessing. We show that employing SAT-based preprocessing via the so-called labelled CNF (LCNF) framework before calling MaxHS can in some cases greatly degrade the performance of the solver. As a remedy, we propose a lifting of MaxHS that works directly on LCNFs, allowing for a tighter integration of SAT-based preprocessing and MaxHS. Our empirical results on standard crafted and industrial weighted partial MaxSAT Evaluation benchmarks show overall improvements over the original MaxHS algorithm both with and without SAT-based preprocessing.

上一篇:Mechanism Design and Implementation for Lung Exchange? Suiqian Luo and Pingzhong Tang

下一篇:On the Resiliency of Unit Propagation to Max-Resolution Andre? Abrame? and Djamal Habet

用户评价
全部评价

热门资源

  • Multi-Source Cros...

    Modern NLP applications have enjoyed a great bo...

  • Reference Network...

    Neural Machine Translation (NMT) has achieved n...

  • Soft Contextual D...

    While data augmentation is an important trick t...

  • Style Transformer...

    Disentangling the content and style in the lat...

  • Towards Fine-grai...

    In this paper, we focus on the task of finegra...