SATenstein: Automatically building local search SAT solvers from components

详细信息    查看全文

• 作者：Ashiqur R. KhudaBukhsh^a ; ¹ ; ^{akhudabu@cs.cmu.edu" class="auth_mail" title="E-mail the corresponding author} ; Lin Xu^b ; ¹ ; ^{xulin730@cs.ubc.ca" class="auth_mail" title="E-mail the corresponding author} ; Holger H. Hoos^b ; ^{hoos@cs.ubc.ca" class="auth_mail" title="E-mail the corresponding author} ; Kevin Leyton-Brown^b ; ^{kevinlb@cs.ubc.ca" class="auth_mail" title="E-mail the corresponding author}
• 关键词：SAT ; Stochastic local search ; Automatic algorithm configuration
• 刊名：Artificial Intelligence
• 出版年：2016
• 出版时间：March 2016
• 年：2016
• 卷：232
• 期：Complete
• 页码：20-42
• 全文大小：784 K

文摘

Designing high-performance solvers for computationally hard problems is a difficult and often time-consuming task. Although such design problems are traditionally solved by the application of human expertise, we argue instead for the use of automatic methods. In this work, we consider the design of stochastic local search (SLS) solvers for the propositional satisfiability problem (SAT). We first introduce a generalized, highly parameterized solver framework, dubbed SATenstein, that includes components drawn from or inspired by existing high-performance SLS algorithms for SAT. The parameters of SATenstein determine which components are selected and how these components behave; they allow SATenstein to instantiate many high-performance solvers previously proposed in the literature, along with trillions of novel solver strategies. We used an automated algorithm configuration procedure to find instantiations of SATenstein that perform well on several well-known, challenging distributions of SAT instances. Our experiments show that SATenstein solvers achieved dramatic performance improvements as compared to the previous state of the art in SLS algorithms; for many benchmark distributions, our new solvers also significantly outperformed all automatically tuned variants of previous state-of-the-art algorithms.