TY - GEN
T1 - Validating the result of a Quantified Boolean Formula(QBF) solver
T2 - 2005 Asia and South Pacific Design Automation Conference, ASP-DAC 2005
AU - Yu, Yinlei
AU - Malik, Sharad
PY - 2005
Y1 - 2005
N2 - 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 unsatishable QBF instances.
AB - 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 unsatishable QBF instances.
UR - http://www.scopus.com/inward/record.url?scp=38049178086&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38049178086&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:38049178086
SN - 0780387368
SN - 9780780387362
T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
SP - 1047
EP - 1051
BT - Proceedings of the 2005 Asia and South Pacific Design Automation Conference, ASP-DAC 2005
Y2 - 18 January 2005 through 21 January 2005
ER -