We demonstrate how to learn efficient heuristics for automated reasoning algorithms through deep reinforcement learning. We focus on backtracking search algorithms for quantified Boolean logics, which already can solve formulas of impressive size -up to 100s 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 challenging problems, the heuristic learned through our approach reduces execution time by a factor of 10 compared to the existing handwritten heuristics.
The paper proposes an approach to automatically learning variable selection
heuristics for QBF using deep learning. The evaluation presented by the authors
shows the promise of the method and demonstrates significant performance
improvements over a variable selection heuristic that does not use machine
learning.
In practice, the overhead of the proposed method is likely to be a major
obstacle in its adoption. The authors note the difficulty of finding suitable
benchmarks and restrict the set of instances they use for evaluation to formulae
where the proposed method is likely to achieve improvements. This skews the
evaluation in favor of the proposed method; in particular, the 90% improvement
figure mentioned in the abstract is not representative of the general case.
Indeed, on another set of instances the proposed method falls significantly
short of the performance of a state-of-the-art heuristic that does not employ
learning.
A drawback of the paper is that there is no comparison to related work. I
realize that this is difficult to achieve because other approaches are in
related, but different areas and may be difficult to adapt for this case, but a
general comparison to the improvements other approaches achieve would be
helpful.
Nevertheless, the work is interesting and presents a new angle on using machine
learning to speed up combinatorial problem solving. While several issues hinder
practical adoption, this is likely to lead to interesting follow-up work that
will improve problem solving in practice.
The description of the method (Section 4.1) is short and not detailed enough to
reproduce the approach the authors are proposing. However, the code is
available.
In summary, I feel that the paper can be accepted.