Validating the result of a Quantified Boolean Formula(QBF) solver: Theory and practice

Yinlei Yu, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

28 Scopus citations

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 unsatishable QBF instances.

Original languageEnglish (US)
Title of host publicationProceedings of the 2005 Asia and South Pacific Design Automation Conference, ASP-DAC 2005
Pages1047-1051
Number of pages5
StatePublished - Dec 1 2005
Event2005 Asia and South Pacific Design Automation Conference, ASP-DAC 2005 - Shanghai, China
Duration: Jan 18 2005Jan 21 2005

Publication series

NameProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
Volume2

Other

Other2005 Asia and South Pacific Design Automation Conference, ASP-DAC 2005
CountryChina
CityShanghai
Period1/18/051/21/05

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Cite this

Yu, Y., & Malik, S. (2005). Validating the result of a Quantified Boolean Formula(QBF) solver: Theory and practice. In Proceedings of the 2005 Asia and South Pacific Design Automation Conference, ASP-DAC 2005 (pp. 1047-1051). [1466520] (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2).