QBF Solving: Advantages and disadvantages of different approaches

Abstract:

Boolean satisfiability (SAT) is believed to be hard in the worst case. However, many heuristic based software can solve industrial SAT instances with tens of thousands of variables in a reasonable amount of time. Theoretical study of these heuristics helps us in understanding the type of formulas these software can and can’t solve in polynomial time, and in comparing different software.

Motivated by the success of SAT solving software, software have been created for an even harder problem: checking whether a Quantified Boolean Formula (QBF) is true or false. We will survey some of these heuristics and compare them with each other.