Certified Symmetry and Dominance Breaking for Combinatorial Optimisation

要約

対称性と支配性の破れは、難しい組み合わせ検索や最適化の問題を解決するために重要ですが、これらの手法の正しさは微妙な議論に依存することがあります。
このため、解が正しく計算されたことを証明する、効率的で機械検証可能な証明書を作成することが望ましいです。
切断面証明システムに基づいて、対称性と支配性の破れを簡単に表現できる最適化問題の証明方法を開発します。
私たちの実験的評価は、ブール充足可能性 (SAT) 解法で完全に一般的な対称性の破れを効率的に検証できることを実証し、XOR と基数推論も含む一連の高度な SAT 技術を証明するための統一された方法を初めて提供します。
さらに、このアプローチがより広範囲の組み合わせ問題に適用できるという概念の実証として、私たちの方法を最大クリーク解決と制約プログラミングに適用します。

要約(オリジナル)

Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes XOR and cardinality reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google