Branching rules for satisfiability analysed with factor analysis

Factor analysis is a statistical technique for reducing the number of factors responsible for a matrix of correlations to a smaller number of factors that may reflect underlying variables. Earlier experiments with constraint satisfaction problems (CSPs) using factor analysis suggested that there are only a few distinct principles of heuristic action. Here, this work is extended to the analysis of branching rules for SAT problems using the Davis-Putnam algorithm. These experiments show that just as with CSPs, there seem to be two basic actions that distinguish heuristics, characterised as building up of contention and propagation of effects to the uninstantiated portion of the problem.