“Search trees”, “branching trees”, “backtracking trees” or “enumeration trees” are at the heart of many (complete) approaches towards hard combinatorial problems, constraint problems, and, of course, SAT problems. Given many choices for branching, the fundamental question is how to guide the choices so that the resulting trees are (relatively) small. Despite (or perhaps because) of its apparently more narrow scope, especially in the SAT area several approaches from theory and applications have found together, and the rudiments of a theory of branching heuristics emerged. In this chapter the first systematic treatment is given.
So a general theory of heuristics guiding the construction of “branching trees” is developed, ranging from a general theoretical analysis to the analysis of the historical development of branching heuristics for SAT solvers, and also to heuristics beyond SAT solving.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com