Matthew L. Ginsberg, David A. McAllester
There has been substantial recent interest in two new families of search techniques. One family consists of nonsystematic methods such as GSAT; the other contoi-~ systematic approaches that use a polynomial amount of justification information to prune the search space. This paper introduces a new technique that combines these two approaches. The algorithm allows substantial freedom of movement in the search space but enough information is retained to ensure the systematicity of the resulting analysis. The size of the justification database is guaranteed to be polynomial in the size of the problem in question.