Name
Abstract | ||
|---|---|---|
We propose subsumed label elimination (SLE), a so-called label-based preprocessing technique for the Boolean optimization paradigm of maximum satisfiability (MaxSAT). We formally show that SLE is orthogonal to previously proposed SAT-based preprocessing techniques for MaxSAT in that it can simplify the underlying minimal unsatisfiable core structure of MaxSAT instances. We also formally show that SLE can considerably reduce the number of internal SAT solver calls within modern core-guided MaxSAT solvers. Empirically, we show that combining SLE with SAT-based preprocessing improves the performance of various state-of-the-art MaxSAT solvers on standard industrial weighted partial MaxSAT benchmarks. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.3233/978-1-61499-672-9-630 | Frontiers in Artificial Intelligence and Applications |
Field | DocType | Volume |
Computer science,Satisfiability,Theoretical computer science | Conference | 285 |
ISSN | Citations | PageRank |
0922-6389 | 1 | 0.36 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeremias Berg | 1 | 41 | 7.87 |
| Paul Saikko | 2 | 33 | 3.98 |
| Matti Järvisalo | 3 | 581 | 51.00 |