ghostq-cegar

Submitter: William Klieber
Description: Devised by W. Klieber, is a non-prenex DPLL-based solver which makes use of auxiliary variables to force necessary assignments, i.e., to force a value to an existential (resp. universal) variable if the opposite value directly makes the formula evaluate to false (resp. true).
It features a counterexample guided abstraction refinement (CEGAR) based learning to further prune the search space when the last decision literal is existential (resp. universal) and a conflict (resp. solution) is detected.
Details are available in
Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Theory and Applications of Satisfiability Testing– SAT 2010. Springer (2010) 128–142
Results: