Partial Maximum Satisfiability (PMS) is a generalisation of the well-known Maximum Satisfiability (MaxSAT), incorporating both hard and soft clauses. Weighted Partial Maximum Satisfiability (WPMS) further extends PMS by associating each soft clause with a positive integer weight. WPMS is particularly significant in practical applications, as it can encode numerous industrial optimisation problems involving hard constraints and soft constraints with varying priorities. Stochastic local search (SLS) algorithms have been extensively studied for solving WPMS, which has achieved significant advancements in recent years. In this work, we identify two issues in current SLS solvers and propose a corresponding solution. Firstly, we observe that current SLS solvers typically employ a fixed initialisation procedure at the start of each local search round, which may restrict the diversity of search directions. Secondly, current SLS solvers often fail to effectively utilise historical information. To address these issues, we propose a novel clause initialisation method that dynamically adjusts the weights of soft clauses based on both the current search state and historical information. Based on this method, we develop a new SLS solver for WPMS named HistLS. Extensive experiments on WPMS benchmarks from the incomplete track of MaxSAT Evaluations (MSEs) of the five recent years demonstrate that HistLS outperforms state-of-the-art SLS solvers.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Improving Local Search for Weighted Partial MaxSAT by Initializing with Historical Information

  • Menghua Jiang,
  • Rui Zhang,
  • Yin Chen

摘要

Partial Maximum Satisfiability (PMS) is a generalisation of the well-known Maximum Satisfiability (MaxSAT), incorporating both hard and soft clauses. Weighted Partial Maximum Satisfiability (WPMS) further extends PMS by associating each soft clause with a positive integer weight. WPMS is particularly significant in practical applications, as it can encode numerous industrial optimisation problems involving hard constraints and soft constraints with varying priorities. Stochastic local search (SLS) algorithms have been extensively studied for solving WPMS, which has achieved significant advancements in recent years. In this work, we identify two issues in current SLS solvers and propose a corresponding solution. Firstly, we observe that current SLS solvers typically employ a fixed initialisation procedure at the start of each local search round, which may restrict the diversity of search directions. Secondly, current SLS solvers often fail to effectively utilise historical information. To address these issues, we propose a novel clause initialisation method that dynamically adjusts the weights of soft clauses based on both the current search state and historical information. Based on this method, we develop a new SLS solver for WPMS named HistLS. Extensive experiments on WPMS benchmarks from the incomplete track of MaxSAT Evaluations (MSEs) of the five recent years demonstrate that HistLS outperforms state-of-the-art SLS solvers.