要約
対称性の破れは、SATやMIPのような制約プログラミングのソルバーを強化するための広く普及しているアプローチである。対称性の破れ述語(SBP)は、一般的に変数に順序を課し、代入の各軌道における辞書的リーダ(lexicographic leader)を選び出す。完全なlex-leader SBPを見つけることはNP困難であるが、不完全なlex-leader SBPは実際に広く使われている。 本論文では、SATの完全なSBPを計算する複雑さについて調べる。我々の主な結果は、SBPを効率的に計算するための自然な障壁である、グラフ非同型性の効率的な証明を証明するものである。我々の結果は、行-列対称性を持つ行列モデルやグラフ生成問題などの重要なCP問題において、短いSBPを得ることが困難であることを説明する。我々の結果は、SBPに追加の変数を導入することが許される場合でも成り立つ。また、ある種の対称群、すなわち木の自動多相性群や群の輪積を効率的なSBPで解くための多項式上限を示す。
要約(オリジナル)
Symmetry breaking is a widely popular approach to enhance solvers in constraint programming, such as those for SAT or MIP. Symmetry breaking predicates (SBPs) typically impose an order on variables and single out the lexicographic leader (lex-leader) in each orbit of assignments. Although it is NP-hard to find complete lex-leader SBPs, incomplete lex-leader SBPs are widely used in practice. In this paper, we investigate the complexity of computing complete SBPs, lex-leader or otherwise, for SAT. Our main result proves a natural barrier for efficiently computing SBPs: efficient certification of graph non-isomorphism. Our results explain the difficulty of obtaining short SBPs for important CP problems, such as matrix-models with row-column symmetries and graph generation problems. Our results hold even when SBPs are allowed to introduce additional variables. We show polynomial upper bounds for breaking certain symmetry groups, namely automorphism groups of trees and wreath products of groups with efficient SBPs.
arxiv情報
| 著者 | Markus Anders,Sofia Brenner,Gaurav Rattan |
| 発行日 | 2024-07-05 11:09:55+00:00 |
| arxivサイト | arxiv_id(pdf) |