In this paper, we present an efficient global-search strat-gey in an algorithm based on the theory of discrete La-grange multipliers for solving difficult SAT instances. These difficult benchmarks generally have many trps and basins that attract local-search trajectories. In contrast to trap-escaping strategies proposed earlier (Wu & Wah 1999a; 1999b) that only focus on traps, we propose a global-search strategy that penalizes a search for visiting points close to points visited before in the trajectory, where peralties are computed based on the Hmming distances between the cur-rent and historical points in the trajectory. The new strat-egy specializes to the earlier trap-escaping strategies because when a trajectory is inside a trap, its historical information will contain many points in close vicinity to each other. It is, however, more general than trap escaping be-cause it tries to avoid visiting the same region repeatedly even when the trajectory is not inside a trap. By comparing our results to existing results in the area (Wu & Stuckey 1998a; 1999b; Kautz & Selman 1996; Coi, Lee, & Stuckey 1998; Marques-Silva & Sakalla 1999), we conclude that our pro-posed strategy is both effective and general.
展开▼
