QBF Solving: Advantages and disadvantages of different approachesSpeaker: Gaurav Sood, IMSc, ChennaiTime: 5PM, 13th October, 2021
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.