Solving QBF by Clause Selection

Abstract

Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. This paper exploits enumeration of implicit hitting sets in the context of Quantified Boolean Formulas (QBF). The paper starts by developing a simple algorithm for QBF with two levels of quantification, which is shown to relate with existing work on enumeration of implicit hitting sets, but also with recent work on QBF based on abstraction refinement. The paper then extends these ideas and develops a novel QBF algorithm, which generalizes the concept of enumeration of implicit hitting sets. Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving.

References in corpus (1)

• Solving QBF with Counterexample Guided Refinement

Cited by in corpus (7)

• Evaluating QBF Solvers: Quantifier Alternations Matter
• Propositional Abduction with Implicit Hitting Sets
• Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
• Expansion-Based QBF Solving Without Recursion
• PrideMM: A Solver for Relaxed Memory Models
• Understanding and Extending Incremental Determinization for 2QBF
• Clausal Abstraction for DQBF (full version)