×

zbMATH — the first resource for mathematics

Combining adaptive noise and look-ahead in local search for SAT. (English) Zbl 1214.68362
Marques-Silva, João (ed.) et al., Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72787-3/pbk). Lecture Notes in Computer Science 4501, 121-133 (2007).
Summary: The adaptive noise mechanism was introduced in Novelty+ to automatically adapt noise settings during the search. The local search algorithm G\( ^{2}\)WSAT deterministically exploits promising decreasing variables to reduce randomness and consequently the dependence on noise parameters. In this paper, we first integrate the adaptive noise mechanism in G\( ^{2}\)WSAT to obtain an algorithm adaptG\( ^{2} \)WSAT, whose performance suggests that the deterministic exploitation of promising decreasing variables cooperates well with this mechanism. Then, we propose an approach that uses look-ahead for promising decreasing variables to further reinforce this cooperation. We implement this approach in adaptG\( ^{2}\)WSAT, resulting in a new local search algorithm called adaptG\( ^{2} \)WSAT\( _{\text{P}}\). Without any manual noise or other parameter tuning, adaptG\( ^{2} \)WSAT\( _{\text{P}}\) shows generally good performance, compared with G\( ^{2} \)WSAT with approximately optimal static noise settings, or is sometimes even better than G\(^{2} \)WSAT. In addition, adaptG\( ^{2} \)WSAT\( _{\text{P} }\) is favorably compared with state-of-the-art local search algorithms such as R+adaptNovelty+ and VW.
For the entire collection see [Zbl 1120.68007].

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
UBCSAT
PDF BibTeX XML Cite
Full Text: DOI