对SAT求解器中重新启动的复杂性理论理解
Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
摘要：
重新启动是一种广泛使用的技术，它与逻辑驱动子句学习（CDCL）布尔SAT求解器的效率密不可分。虽然这些政策的效用已经很好地建立了经验，理论上的解释是否重新启动确实是至关重要的CDCL解决方案的力量是缺乏的。在本文中，我们证明了一系列的理论结果，表征的权力重新启动各种型号的SAT求解器。更准确地说，我们做出了以下贡献。首先，我们证明了一个{ \it drunk}随机CDCL求解器模型之间的指数分离的重新启动和相同的模型没有重新启动使用一个家庭的可满足的实例。其次，我们表明，配置的CDCL求解器VSIDS分支和重新启动（与活动重新启动后擦除）是指数比相同的配置没有重新启动一个家庭的不可满足的实例更强大。据我们所知，这些是第一个分离的结果，涉及重新启动的情况下，SAT求解器。第三，我们表明，重新启动不增加任何证明复杂性理论的权力相对于一些模型的CDCL和DPLL求解器与非确定性的静态变量和值的选择。
英文摘要：
Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical explanation of whether restarts are indeed crucial to the power of CDCL solvers is lacking. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a {\it drunk} randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
