Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. Pages 824-830.
Abstract
Many AI-related reasoning problems are based on the problem of satisfiability (SAT). While SAT itself becomes easy when restricting the structure of the formulas in a certain way, this is not guaranteed for more involved reasoning problems. In this work, we focus on reasoning tasks in the areas of belief revision and logic-based abduction and show that in some cases the restriction to Krom formulas (i.e., formulas in CNF where clauses have at most two literals) decreases the complexity, while in others it does not. We thus also consider additional restrictions to Krom formulas towards a better identification of the tractability frontier of such problems.
@inproceedings{ijcai2013p128,
title = {Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?},
author = {Creignou, Nadia and Pichler, Reinhard and Woltran, Stefan},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on
Artificial Intelligence, {IJCAI-13}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Francesca Rossi},
pages = {824--830},
year = {2013},
month = {8},
url = {https://ijcai.org/proceedings/2013/128},
}
TY - CPAPER TI - Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment? AU - Creignou, Nadia AU - Pichler, Reinhard AU - Woltran, Stefan T2 - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2013 SP - 824 EP - 830 UR - https://ijcai.org/proceedings/2013/128 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
