Solving QBF by Clause Selection
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 325-330.
Abstract
Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. This paper exploits enumeration of implicit hitting sets in the context of Quantified Boolean Formulas (QBF). The paper starts by developing a simple algorithm for QBF with two levels of quantification, which is shown to relate with existing work on enumeration of implicit hitting sets, but also with recent work on QBF based on abstraction refinement. The paper then extends these ideas and develops a novel QBF algorithm, which generalizes the concept of enumeration of implicit hitting sets. Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving.
@inproceedings{ijcai2015p52,
title = {Solving QBF by Clause Selection},
author = {Janota, Mikolás and Silva, João P. Marques},
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 = {325--330},
year = {2015},
month = {7},
note = {Main Track},
url = {https://ijcai.org/proceedings/2015/52},
}
TY - CPAPER TI - Solving QBF by Clause Selection AU - Janota, Mikolás AU - Silva, João P. Marques T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 325 EP - 330 UR - https://ijcai.org/proceedings/2015/52 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
