Klaus
Truemper
Title:
An algorithm for Q-ALL SAT with learning via heuristics
Abstract:
Problem Q-ALL SAT is an important logic problem at the second
level of
the polynomial hierarchy. It is a particular case of the quantified
Boolean formulas (QBFs). We describe a solution tree-search algorithm
that learns via heuristics. The scheme is substantially faster than the
fastest competing QBF schemes. The main message of the talk is that (1)
it pays to construct algorithms for specially structured problem
classes (nothing new her for combinatorics), and (2) learning and
heuristics can make a terrific contribution in exact combinatorial
algorithms.