资源论文SATenstein: Automatically Building Local Search SAT Solvers From Components

SATenstein: Automatically Building Local Search SAT Solvers From Components

2019-11-15 | |  70 |   37 |   0

Abstract Designing high-performance algorithms for computationally hard problems is a diffificult and often time-consuming task. In this work, we demonstrate that this task can be automated in the context of stochastic local search (SLS) solvers for the propositional satisfifiability problem (SAT). We fifirst introduce a generalised, highly parameterised solver framework, dubbed SATenstein, that includes components gleaned from or inspired by existing high-performance SLS algorithms for SAT. The parameters of SATenstein control the selection of components used in any specifific instantiation and the behaviour of these components. SATenstein can be confifigured to instantiate a broad range of existing high-performance SLSbased SAT solvers, and also billions of novel algorithms. We used an automated algorithm confifiguration procedure to fifind instantiations of SATenstein that perform well on several well-known, challenging distributions of SAT instances. Overall, we consistently obtained signifificant improvements over the previously best-performing SLS algorithms, despite expending minimal manual effort.1

上一篇:New Improvements in Optimal Rectangle Packing

下一篇:Exploiting Decomposition on Constraint Problems with High Tree-Width

用户评价
全部评价

热门资源

  • The Variational S...

    Unlike traditional images which do not offer in...

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Rating-Boosted La...

    The performance of a recommendation system reli...