Quaig

| project staff | description | benchmarks | publications |

Quaig is a tool which integrates complementary QBF solving techniques using two state-of-the-art solvers as substructure: AIGSolve (variable elimination) and QuBE (search based). There are mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. The tool determines (by estimating the quality) appropriate points in time to store the current partial result during variable elimination and switches from variable elimination to search-based methods when the progress of variable elimination is supposed to be too slow or when representation (the AIG) grow too fast.

Any Quantified Boolean Formula (QBF) in QDimacs format. QBFLIB is the official library of QBF formulas.