Clause Weighting Local Search for SAT

File Size Format
40707.pdf 247Kb Adobe PDF View
Title Clause Weighting Local Search for SAT
Author Thornton, John
Journal Name Journal of Automated Reasoning
Editor Deepak Kapur
Year Published 2006
Place of publication Netherlands
Publisher Springer
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.
Peer Reviewed Yes
Published Yes
Alternative URI http://dx.doi.org/10.1007/s10817-005-9010-1
Copyright Statement Copyright 2006 Springer. This is the author-manuscript version of this paper. Reproduced in accordance with the copyright policy of the publisher. The original publication is available at www.springerlink.com
Volume 35
Page from 97
Page to 142
ISSN 0168-7433
Date Accessioned 2007-03-09
Language en_AU
Research Centre Institute for Integrated and Intelligent Systems
Faculty Faculty of Engineering and Information Technology
Subject PRE2009-Other Artificial Intelligence
URI http://hdl.handle.net/10072/13781
Publication Type Journal Articles (Refereed Article)
Publication Type Code c1

Show simple item record

Griffith University copyright notice