Extracting Certificates from Quantified Boolean Formulas
Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence. Pages 47-52.
Abstract
A certificate of satisfiability for a quantified boolean formula is a compact representation of one of its models which is used to provide solverindependent evidence of satisfiability. In addition, it can be inspected to gather explicit information about the semantics of the formula. Due to the intrinsic nature of quantified formulas, such certificates demand much care to be efficiently extracted, compactly represented, and easily queried. We show how to solve all these problems.
Marco Benedetti. 2005. Extracting Certificates from Quantified Boolean Formulas. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI-05. IJCAI, 47–52. https://ijcai.org/proceedings/2005/118
Benedetti, M. (2005). Extracting Certificates from Quantified Boolean Formulas. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI-05 (pp. 47–52). IJCAI. https://ijcai.org/proceedings/2005/118
@inproceedings{ijcai2005p118,
title = {Extracting Certificates from Quantified Boolean Formulas},
author = {Benedetti, Marco},
booktitle = {Proceedings of the Nineteenth International Joint Conference on
Artificial Intelligence, {IJCAI-05}},
publisher = {International Joint Conferences on Artificial Intelligence},
pages = {47--52},
year = {2005},
url = {https://ijcai.org/proceedings/2005/118},
}
TY - CPAPER TI - Extracting Certificates from Quantified Boolean Formulas AU - Benedetti, Marco T2 - Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI-05 PB - International Joint Conferences on Artificial Intelligence PY - 2005 SP - 47 EP - 52 UR - https://ijcai.org/proceedings/2005/118 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
