Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT

Berg, Jeremias; Saikko, Paul; Järvisalo, Matti

Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT

Jeremias Berg, Paul Saikko, Matti Järvisalo

Download BibTeX Cite

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 239-244.

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.

Jeremias Berg, Paul Saikko, and Matti Järvisalo. 2015. Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15. IJCAI, 239–244. https://ijcai.org/proceedings/2015/40

@inproceedings{ijcai2015p40,
  title     = {Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT},
  author    = {Berg, Jeremias and Saikko, Paul and Järvisalo, Matti},
  booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
               Artificial Intelligence, {IJCAI-15}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Qiang Yang and Michael Wooldridge},
  pages     = {239--244},
  year      = {2015},
  month     = {7},
  note      = {Main Track},
  url       = {https://ijcai.org/proceedings/2015/40},
}

TY  - CPAPER
TI  - Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT
AU  - Berg, Jeremias
AU  - Saikko, Paul
AU  - Järvisalo, Matti
T2  - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15
PB  - International Joint Conferences on Artificial Intelligence
PY  - 2015
SP  - 239
EP  - 244
UR  - https://ijcai.org/proceedings/2015/40
ER  -