Stochastic Local Search Methods for Dynamic SAT - an Initial Investigation

We introduce the dynamic SAT problem, a generalisation of the satisfiability problem in propositional logic which allows changes of a problem over time. DynSAT can be seen as a particular form of a dynamic CSP, but considering results and recent success in solving conventional SAT problems, we believe that the conceptual simplicity of SAT will allow us to more easily devise and investigate high-performing algorithms for DynSAT than for dynamic CSPs. In this article, we motivate the DynSAT problem, discuss various formalisations of it, and investigate stochastic local search (SLS) algorithms for solving it. In particular, we apply SLS algorithms which perform well on conventional SAT problems to dynamic problems and we analyse and characterise their performance empirically; this initial investigation indicates that the performance differences between various algorithms of the well-known WalkSAT family of SAT algorithms generally carry over when applied to DynSAT. We also study different generic approaches of solving DynSAT problems using SLS algorithms and investigate their performance differences when applied to different types of DynSAT problems.