Maximum Satisfiability Using Cores and Correction Sets
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 246-251.
Abstract
Core-guided MAXSAT algorithms dominate other methods in solving industrial MAXSAT problems. In this work, we propose a new efficient algorithm that is guided by correction sets and cores. At every iteration, the algorithm obtains a correction set or a core, which is then used to rewrite the formula using incremental and succinct transformations. We theoretically show that correction sets and cores have complementary strengths and empirically demonstrate that their combination leads to an efficient MAXSAT solver that outperforms state-of-the-art WPMS solvers on the 2014 Evaluation on industrial instances.
@inproceedings{ijcai2015p41,
title = {Maximum Satisfiability Using Cores and Correction Sets},
author = {Bjørner, Nikolaj S. and Narodytska, Nina},
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 = {246--251},
year = {2015},
month = {7},
note = {Main Track},
url = {https://ijcai.org/proceedings/2015/41},
}
TY - CPAPER TI - Maximum Satisfiability Using Cores and Correction Sets AU - Bjørner, Nikolaj S. AU - Narodytska, Nina T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 246 EP - 251 UR - https://ijcai.org/proceedings/2015/41 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
