Counting the number of solutions of true and false quantified Boolean formulas (QBFs) has received increased interest in recent years. However, the explicit enumeration of all solutions for a QBF is almost unexplored so far. For QBF solution counting, it has been shown that enumeration-based counting as employed in SAT is not complete for QBF. Solution enumeration runs into the same problem. We propose a refinement-based approach to enumerate (all) solutions of true and false QBFs. To this end, we develop a novel framework to characterize the enumeration problem at quantifier level two and present a complete enumeration algorithm that can be interrupted at any time as soon as enough solutions are found. We evaluated our implementation called QEnum in three different case studies.

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

Refinement-Based Enumeration of QBF Solutions

  • Andreas Plank,
  • Clemens Hofstadler,
  • Maximilian Heisinger,
  • Martina Seidl

摘要

Counting the number of solutions of true and false quantified Boolean formulas (QBFs) has received increased interest in recent years. However, the explicit enumeration of all solutions for a QBF is almost unexplored so far. For QBF solution counting, it has been shown that enumeration-based counting as employed in SAT is not complete for QBF. Solution enumeration runs into the same problem. We propose a refinement-based approach to enumerate (all) solutions of true and false QBFs. To this end, we develop a novel framework to characterize the enumeration problem at quantifier level two and present a complete enumeration algorithm that can be interrupted at any time as soon as enough solutions are found. We evaluated our implementation called QEnum in three different case studies.