Extracting Certificates from Quantified Boolean Formulas
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. 1
Cite
Text
Benedetti. "Extracting Certificates from Quantified Boolean Formulas." International Joint Conference on Artificial Intelligence, 2005.Markdown
[Benedetti. "Extracting Certificates from Quantified Boolean Formulas." International Joint Conference on Artificial Intelligence, 2005.](https://mlanthology.org/ijcai/2005/benedetti2005ijcai-extracting/)BibTeX
@inproceedings{benedetti2005ijcai-extracting,
title = {{Extracting Certificates from Quantified Boolean Formulas}},
author = {Benedetti, Marco},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2005},
pages = {47-53},
url = {https://mlanthology.org/ijcai/2005/benedetti2005ijcai-extracting/}
}