Paper Info
Title
Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice
Abstract
Despite the increasing use of QBF solvers, current QBF solvers do not provide for any mechanism to verify their results. This paper demonstrates a methodology for independently validating the results of a DLL based QBF solver using the traces generated during the solving process. It also presents a mechanism to extract small unsatisfiable subformulas, called cores, from unsatisfiable QBF instances.
Year
DOI
Venue
2005
10.1145/1120725.1120821
ASP-DAC
Keywords
Field
DocType
unsatisfiable qbf instance,quantified boolean formula,small unsatisfiable subformulas,current qbf solvers,qbf solvers,qbf solver,increasing use,boolean functions,computability,interconnect,tdm
Boolean function,Partial product,Computer science,Algorithm,Computability,Electronic engineering,Theoretical computer science,Solver,True quantified Boolean formula
Conference
ISSN
ISBN
Citations 
2153-6961
0-7803-8737-6
25
PageRank 
References 
Authors
1.19
15
2
Name
Order
Citations
PageRank
Yinlei Yu1955.96
Sharad Malik27766691.24