Clause Weighting Local Search for SAT |
| |
Authors: | John Thornton |
| |
Affiliation: | (1) Institute for Integrated and Intelligent Systems, Griffith University, PMB 50, Gold Coast Mail Centre, Queensland, 9726, Australia |
| |
Abstract: | This paper investigates the necessary features of an effective clause weighting local search algorithm for propositional satisfiability
testing. Using the recent history of clause weighting as evidence, we suggest that the best current algorithms have each discovered
the same basic framework, that is, to increase weights on false clauses in local minima and then to periodically normalize
these weights using a decay mechanism. Within this framework, we identify two basic classes of algorithm according to whether
clause weight updates are performed additively or multiplicatively. Using a state-of-the-art multiplicative algorithm (SAPS) and our own pure additive weighting scheme (PAWS), we constructed
an experimental study to isolate the effects of multiplicative in comparison to additive weighting, while controlling other
key features of the two approaches, namely, the use of pure versus flat random moves, deterministic versus probabilistic weight smoothing and multiple versus single inclusion of literals in the local search neighbourhood. In addition, we examined the effects of adding a threshold
feature to multiplicative weighting that makes it indifferent to similar cost moves. As a result of this investigation, we
show that additive weighting can outperform multiplicative weighting on a range of difficult problems, while requiring considerably
less effort in terms of parameter tuning. Our examination of the differences between SAPS and PAWS suggests that additive
weighting does benefit from the random flat move and deterministic smoothing heuristics, whereas multiplicative weighting
would benefit from a deterministic/probabilistic smoothing switch parameter that is set according to the problem instance.
We further show that adding a threshold to multiplicative weighting produces a general deterioration in performance, contradicting
our earlier conjecture that additive weighting has better performance due to having a larger selection of possible moves.
This leads us to explain differences in performance as being mainly caused by the greater emphasis of additive weighting on
penalizing clauses with relatively less weight. |
| |
Keywords: | constraint satisfaction satisfiability local search |
本文献已被 SpringerLink 等数据库收录! |
|