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
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
Titolo: | Hybrid Evaluation Procedures for QBF |
Autori: | |
Data di pubblicazione: | 2005 |
Rivista: | |
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 |
Handle: | http://hdl.handle.net/11582/2632 |
Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.