论文标题
Bandmaxsat:一款本地搜索Maxsat求解器,带有多臂强盗
BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit
论文作者
论文摘要
我们解决了部分MaxSAT(PMS)和加权PMS(WPM),这是MaxSat问题的两个实际概括,并为这些问题(称为BandMaxSat)提出了一种局部搜索算法,该算法应用了多武器的强盗模型来指导搜索方向。我们方法中的强盗与输入(W)PMS实例中的所有软从句相关联。每个手臂对应于一个软子句。 Bandit模型可以帮助BandMaxSat选择一个良好的方向,以通过在当前步骤中选择要满足的软子句,即选择要拉的手臂,从而逃脱了本地Optima。我们进一步提出了一种初始化方法(w)PMS,该方法在生产初始解决方案时优先考虑单位和二进制子句。广泛的实验表明,BandMaxSat显着超过了最先进的(W)PMS本地搜索算法SATLIKE3.0。具体而言,BandMaxSat获得更好结果的实例数量大约是Satlike3.0获得的两倍。此外,我们将bandmaxsat与完整的求解器tt-open-wbo-inc相结合。由此产生的求解器bandmaxsat-c还表现出一些最好的最先进的完整(W)PMS求解器,包括satlike-c,loandra和tt-open-wbo-inc。
We address Partial MaxSAT (PMS) and Weighted PMS (WPMS), two practical generalizations of the MaxSAT problem, and propose a local search algorithm for these problems, called BandMaxSAT, that applies a multi-armed bandit model to guide the search direction. The bandit in our method is associated with all the soft clauses in the input (W)PMS instance. Each arm corresponds to a soft clause. The bandit model can help BandMaxSAT to select a good direction to escape from local optima by selecting a soft clause to be satisfied in the current step, that is, selecting an arm to be pulled. We further propose an initialization method for (W)PMS that prioritizes both unit and binary clauses when producing the initial solutions. Extensive experiments demonstrate that BandMaxSAT significantly outperforms the state-of-the-art (W)PMS local search algorithm SATLike3.0. Specifically, the number of instances in which BandMaxSAT obtains better results is about twice that obtained by SATLike3.0. Moreover, we combine BandMaxSAT with the complete solver TT-Open-WBO-Inc. The resulting solver BandMaxSAT-c also outperforms some of the best state-of-the-art complete (W)PMS solvers, including SATLike-c, Loandra and TT-Open-WBO-Inc.