Co-Certificate Learning with SAT Modulo Symmetries

要約

与えられた co-NP 特性を満たす同型までのすべてのグラフを生成するための新しい SAT ベースの方法を提案します。
私たちの方法は、共同証明書学習と呼ばれる手法を使用して SAT Modulo Symmetry (SMS) フレームワークを拡張します。
SMS が、指定された共同 NP プロパティに違反する候補グラフを生成した場合、この違反に対する証明書、つまり、共同 NP プロパティの「共同証明書」を取得します。
共同証明書により、SMS のバックエンドとして機能する SAT ソルバーが CDCL 手順の一部として学習する条項が生じます。
私たちは、SMS と共同証明書学習が、量子力学の基礎の中心であり、研究されてきた問題である、Kochen-Specker ベクトル系のサイズに関する最もよく知られている下限を改善できる強力な方法であることを実証します。
半世紀以上。
私たちのアプローチは、最近提案された SAT ベースの方法よりも桁違いに高速で、拡張性も大幅に優れています。

要約(オリジナル)

We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i.e., `co-certificate’ for the co-NP property. The co-certificate gives rise to a clause that the SAT solver, serving as SMS’s backend, learns as part of its CDCL procedure. We demonstrate that SMS plus co-certificate learning is a powerful method that allows us to improve the best-known lower bound on the size of Kochen-Specker vector systems, a problem that is central to the foundations of quantum mechanics and has been studied for over half a century. Our approach is orders of magnitude faster and scales significantly better than a recently proposed SAT-based method.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google