GSAT and Dynamic Backtracking

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.