Name
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. |
Year | Venue | DocType |
|---|---|---|
2015 | IJCAI | Conference |
Citations | PageRank | References |
7 | 0.47 | 15 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeremias Berg | 1 | 41 | 7.87 |
| Paul Saikko | 2 | 33 | 3.98 |
| Matti Järvisalo | 3 | 581 | 51.00 |