Quantified Boolean Formulas (QBFs) extend propositional logic with existential and universal quantifiers, making their decision problem PSPACE-hard. Recent advances in QBF solvers have established QBFs as an attractive framework for encoding PSPACE-hard problems across domains such as formal verification, synthesis, and symbolic AI. Despite progress in solving techniques, less attention has been given to the infrastructure for constructing correct and efficient QBF encodings. For instance, it is often unclear whether two QBFs that encode the same problem in different ways yield the same solutions. Traditional QBF equivalence checking focuses only on free variables, yet in many cases, the quantified variables must also be considered. In this paper, we present QSOLE, the first fully automatic checker for solution-based QBF equivalence. Based on a recently introduced approach, QSOLE decomposes equivalence checks into smaller entailment computations and is capable of generating witnesses for detected inequivalences, which can be used to debug encodings. Furthermore, it allows for explicit exclusion of variables from equivalence checks enabling comparison of formulas using different local auxiliary variables.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

QSOLE: Automatic QBF Equivalence Checking

  • Peter Pfeiffer,
  • Mark Peyrer,
  • Daniel Große,
  • Martina Seidl

摘要

Quantified Boolean Formulas (QBFs) extend propositional logic with existential and universal quantifiers, making their decision problem PSPACE-hard. Recent advances in QBF solvers have established QBFs as an attractive framework for encoding PSPACE-hard problems across domains such as formal verification, synthesis, and symbolic AI. Despite progress in solving techniques, less attention has been given to the infrastructure for constructing correct and efficient QBF encodings. For instance, it is often unclear whether two QBFs that encode the same problem in different ways yield the same solutions. Traditional QBF equivalence checking focuses only on free variables, yet in many cases, the quantified variables must also be considered. In this paper, we present QSOLE, the first fully automatic checker for solution-based QBF equivalence. Based on a recently introduced approach, QSOLE decomposes equivalence checks into smaller entailment computations and is capable of generating witnesses for detected inequivalences, which can be used to debug encodings. Furthermore, it allows for explicit exclusion of variables from equivalence checks enabling comparison of formulas using different local auxiliary variables.