---
title: "Extracting Certificates from Quantified Boolean Formulas"
authors:
  - "Marco Benedetti"
doi: ""
url: "https://ijcai.org/proceedings/2005/118"
pdf: "https://ijcai.org/proceedings/2005/0118.pdf"
venue: "Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence"
year: 2005
pages: "47-52"
track: ""
keywords:
---

# Extracting Certificates from Quantified Boolean Formulas

Marco Benedetti

*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.