• DocumentCode
    3548365
  • 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
  • Volume
    2
  • fYear
    2005
  • fDate
    18-21 Jan. 2005
  • Firstpage
    1047
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Design Automation Conference, 2005. Proceedings of the ASP-DAC 2005. Asia and South Pacific
  • Print_ISBN
    0-7803-8736-8
  • Type

    conf

  • DOI
    10.1109/ASPDAC.2005.1466520
  • Filename
    1466520
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3548365