Title :
Validating the result of a quantified Boolean formula (QBF) solver: theory and practice
Author :
Yu, Yinleu ; Malik, Sharad
Author_Institution :
Dept. of Electr. Eng., Princeton Univ., NJ, USA
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.
Keywords :
Boolean functions; computability; QBF solvers; quantified Boolean formula solver; solving process; unsatisfiable subformulas; Artificial intelligence; Automation; Convergence; Logic; Pipelines;
Conference_Titel :
Design Automation Conference, 2005. Proceedings of the ASP-DAC 2005. Asia and South Pacific
Print_ISBN :
0-7803-8736-8
DOI :
10.1109/ASPDAC.2005.1466520
