Clause weighting local search for sat

This paper investigates the necessary features of an effective clause weighting local search algorithm for propositional satisfiability testing. Using the recent his-tory of clause weighting as evidence, we suggest that the best current algorithms have each discovered the same basic framework, i.e. 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 one of the best recently developed multiplicative algorithms (SAPS) and our own pure additive weighting scheme (PAWS), an experimental study was constructed 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 ver-sus flat random moves, deterministic versus probabilistic weight smoothing and multiple versus single inclusion of literals in the local search neighbourhood. I