Invited Talk by Markus Rabe

We are happy to announce that Markus Rabe will be giving an invited talk as part of QBF2020. In the QBF community, Markus is well known for his work on the solvers CAQE and CADET.

In his talk, he will present a paper entitled Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning that has recently been published as part of ICLR 2020.

Here’s the abstract:

We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solve formulas of impressive size - up to hundreds of thousands of variables. The main challenge is to find a representation of these formulas that lends itself to making predictions in a scalable way. For a family of challenging problems, we learned a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.