Integer Linear Programming Preprocessing for Maximum Satisfiability

要約

最大満足度問題（MAXSAT）は、多数の実用的なアプリケーションを備えた主要な最適化の課題です。
最近のMAXSAT評価では、ほとんどのMAXSATソルバーがポートフォリオの一部としてILPソルバーを採用しています。
このペーパーでは、MaxSAT解決に対する整数線形プログラミング（ILP）前処理技術の影響を調査します。
実験結果は、ILP前処理技術が、非加重トラックでのMaxSat評価2024の勝者であるWMAXCDCL-OpenWBO1200を支援することを示しており、15の追加インスタンスを解決します。
さらに、現在の最先端のMAXSATソルバーは、ポートフォリオでILPソルバーを非常に使用していますが、提案されたアプローチにより、WMAXCDCLやMAXCDCLを含むポートフォリオのILPソルバーを呼び出す必要性が減ります。

要約(オリジナル)

The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have adopted an ILP solver as part of their portfolios. This paper investigates the impact of Integer Linear Programming (ILP) preprocessing techniques on MaxSAT solving. Experimental results show that ILP preprocessing techniques help WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 in the unweighted track, solve 15 additional instances. Moreover, current state-of-the-art MaxSAT solvers heavily use an ILP solver in their portfolios, while our proposed approach reduces the need to call an ILP solver in a portfolio including WMaxCDCL or MaxCDCL.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google