SAT Encoding of Partial Ordering Models for Graph Coloring Problems

要約

この論文では、グラフ色分け問題 (GCP) と帯域幅色分け問題 (BCP) に対する部分順序付けベースの ILP モデルの新しい SAT エンコーディングを提案します。
GCP は、隣接する 2 つの頂点がそれぞれ異なる色になるように、特定のグラフの頂点に割り当てることができる色の最小数を要求します。
BCP は一般化したもので、各エッジには割り当てられた色間の「距離」を最小にする重みがあり、目標は使用される「最大の」色を最小限に抑えることです。
広く研究されている GCP について、私たちは新しい SAT エンコーディングを DIMACS ベンチマーク セットの最先端のアプローチと実験的に比較しました。
私たちの評価では、この SAT エンコーディングが疎グラフに対して効果的であり、一部の DIMACS インスタンスでは最先端のエンコーディングを上回るパフォーマンスを発揮することが確認されました。
BCP については、理論分析により、半順序付けベースの SAT および ILP 定式化は、古典的な割り当てベースのモデルよりも漸近的に小さいサイズになることが示されています。
私たちの実際的な評価では、割り当てベースのエンコーディングと比較した優位性だけでなく、一連のベンチマーク インスタンスに対する最先端のアプローチと比較した優位性も確認されました。
私たちの知る限り、私たちは文献から BCP の未解決の事例を初めて解決しました。

要約(オリジナル)

In this paper, we suggest new SAT encodings of the partial-ordering based ILP model for the graph coloring problem (GCP) and the bandwidth coloring problem (BCP). The GCP asks for the minimum number of colors that can be assigned to the vertices of a given graph such that each two adjacent vertices get different colors. The BCP is a generalization, where each edge has a weight that enforces a minimal ‘distance’ between the assigned colors, and the goal is to minimize the ‘largest’ color used. For the widely studied GCP, we experimentally compare our new SAT encoding to the state-of-the-art approaches on the DIMACS benchmark set. Our evaluation confirms that this SAT encoding is effective for sparse graphs and even outperforms the state-of-the-art on some DIMACS instances. For the BCP, our theoretical analysis shows that the partial-ordering based SAT and ILP formulations have an asymptotically smaller size than that of the classical assignment-based model. Our practical evaluation confirms not only a dominance compared to the assignment-based encodings but also to the state-of-the-art approaches on a set of benchmark instances. Up to our knowledge, we have solved several open instances of the BCP from the literature for the first time.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google