Significant advances in practical approaches to maximum satisfiability (MaxSAT) solving have made MaxSAT a viable approach to solving complex NP-hard combinatorial optimization problems. Several recent works have extended single-objective MaxSAT algorithms to the multi-objective setting, enabling the enumeration of Pareto-optimal solutions for problems expressed as multi-objective MaxSAT (MO-MaxSAT). We propose and instantiate an alternative approach to MO-MaxSAT solving. Phrased as an implicit hitting set (IHS) approach, our algorithm works by iteratively invoking a single-objective IHS oracle on a scalarization of the multi-objective instance at hand. Our open-source implementation significantly outperforms an earlier-proposed IHS-style approach and complements the current state of the art in algorithmic approaches to MO-MaxSAT.

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

Multi-objective Maximum Satisfiability by Single-Objective Implicit Hitting Set Optimization

  • Christoph Jabs,
  • Jeremias Berg,
  • Matti Järvisalo

摘要

Significant advances in practical approaches to maximum satisfiability (MaxSAT) solving have made MaxSAT a viable approach to solving complex NP-hard combinatorial optimization problems. Several recent works have extended single-objective MaxSAT algorithms to the multi-objective setting, enabling the enumeration of Pareto-optimal solutions for problems expressed as multi-objective MaxSAT (MO-MaxSAT). We propose and instantiate an alternative approach to MO-MaxSAT solving. Phrased as an implicit hitting set (IHS) approach, our algorithm works by iteratively invoking a single-objective IHS oracle on a scalarization of the multi-objective instance at hand. Our open-source implementation significantly outperforms an earlier-proposed IHS-style approach and complements the current state of the art in algorithmic approaches to MO-MaxSAT.