Stochastic Local Search Methods for Dynamic SAT- an Initial Investigation

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