Abstract: Computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. The well known and most implemented heuristic for quantification scheduling was introduced way in the past in 1995 by Ranjan et. al. Within the last couple of years, this problem has attracted a lots of research, most of which has focussed on scheduling quantifications in image computation equation. This talk brings up to date on many techniques proposed to solve this problem. Naturally, we describe our own methods based on various combinatorial optimization techniques (CHARME'01) and non-linear quantification scheduling using variable scoring heuristics (ICCAD'01). Despite all this research, the problem seems to be as muddled as the BDD variable ordering problem, for which there still is no final satisfactory answer.