A generating function method for the average-case analysis of DPLL

TL;DR

This paper introduces a generating function method to analyze the average size of DPLL search trees for random SAT and graph coloring problems, providing asymptotic estimates based on input parameters and heuristics.

Contribution

It develops a recursive generating function approach to derive asymptotic DPLL search tree sizes for random problems, linking results to problem parameters and heuristics.

Findings

Derives asymptotic growth rates of DPLL search trees as 2^{N w + o(N)}.

Establishes recursion relations for generating functions based on problem parameters.

Provides a framework for analyzing average-case complexity of DPLL algorithms.

Abstract

A method to calculate the average size of Davis-Putnam-Loveland-Logemann (DPLL) search trees for random computational problems is introduced, and applied to the satisfiability of random CNF formulas (SAT) and the coloring of random graph (COL) problems. We establish recursion relations for the generating functions of the average numbers of (variable or color) assignments at a given height in the search tree, which allow us to derive the asymptotics of the expected DPLL tree size, 2^{N w + o(N)}, where N is the instance size. w is calculated as a function of the input distribution parameters (ratio of clauses per variable for SAT, average vertex degree for COL), and the branching heuristics.