Additive versus multiplicative clause weighting for SAT

Abstract

This paper examines the relative performance of additive and multiplicative clause weighting schemes for propositional satisfiability testing.Starting with one of the most recently developed multiplicative algorithms (SAPS), 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 random versus flat moves, deterministic versus probabilistic weight smoothing and multiple versus single inclusion of literals in the local search neighborhood.As a result of this investigation we developed a pure additive weighting scheme (PAWS) which can outperform multiplicative weighting on a range of difficult problems, while requiring considerably less effort in terms of parameter tuning.We conclude that additive weighting shows better scaling properties because it makes less distinction between costs and so considers a larger domain of possible moves.