ghostq-plain
| 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). 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: | |||