Tags:branching, heuristics, look-ahead, theory of SAT solving and trees
Abstract:
We consider a fundamental problem in the theory of branching heuristics for tree-based solvers, applicable e.g. to SAT, #SAT, CSP, #CSP. Such tree-based solvers are used as the cubing-part in the Cube-and-Conquer paradigm, and are thus of renewed interest for general (#)SAT solving. These solvers build at least implicitly a branching (backtracking) tree, with the goal to minimise tree-size. The heuristics consider a transition from an instance F to some "simplified" F', and evaluate the progress by a distance d(F,F'), the bigger the better. When a branching (F_1', ..., F_k') is to be chosen for F, for each possibility we consider its branching tuple t given by t_i = d(F, F_i'), project it to a single number pi(t), and choose a branching with minimal pi(t). This paper investigates the choices for pi(t), in a theoretical framework.
Projection heuristics for binary branchings between sum and product