A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Special Track on Knowledge Representation and Reasoning. Pages 2677-2682.
Abstract
Core-guided algorithms proved to be effective on industrial instances of MaxSAT, the optimization variant of the satisfiability problem for propositional formulas. These algorithms work by iteratively checking satisfiability of a formula that is relaxed at each step by using the information provided by unsatisfiable cores. The paper introduces a new core-guided algorithm that adds cardinality constraints for each detected core, but also limits the number of literals in each constraint in order to control the number of refutations in subsequent satisfiability checks. The performance gain of the new algorithm is assessed on the industrial instances of the 2014 MaxSAT Evaluation.
@inproceedings{ijcai2015p379,
title = {A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size},
author = {Alviano, Mario and Dodaro, Carmine and Ricca, Francesco},
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 = {2677--2682},
year = {2015},
month = {7},
note = {Special Track on Knowledge Representation and Reasoning},
url = {https://ijcai.org/proceedings/2015/379},
}
TY - CPAPER TI - A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size AU - Alviano, Mario AU - Dodaro, Carmine AU - Ricca, Francesco T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 2677 EP - 2682 UR - https://ijcai.org/proceedings/2015/379 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
