Finding hardness reductions automatically using SAT solvers

要約

この記事では、完了問題、つまり部分構造を完全な構造に完成させることができるかどうかの決定問題が、多くの組み合わせ構造に対して NP 完全であることを示します。
文献のほとんどの削減のためのガジェットは手動で見つけられますが、完全に自動化された方法でガジェットを構築するアルゴリズムを紹介します。
SAT に基づくフレームワークを使用して、補完問題が NP 完全である数千の構造を分類することにより、禁止された部分構造を伴う符号マッピングに関する補完問題の最初の徹底的な研究を提示します。
私たちのリストには特に、平面点構成の公理化に向けて Knuth によって導入された内部トリプル システムが含まれています。
最後になりましたが、完成問題が NP 完全である内部三重系を高次元に一般化する構造の無限族を与えます。

要約(オリジナル)

In this article, we show that the completion problem, i.e. the decision problem whether a partial structure can be completed to a full structure, is NP-complete for many combinatorial structures. While the gadgets for most reductions in literature are found by hand, we present an algorithm to construct gadgets in a fully automated way. Using our framework which is based on SAT, we present the first thorough study of the completion problem on sign mappings with forbidden substructures by classifying thousands of structures for which the completion problem is NP-complete. Our list in particular includes interior triple systems, which were introduced by Knuth towards an axiomatization of planar point configurations. Last but not least, we give an infinite family of structures generalizing interior triple system to higher dimensions for which the completion problem is NP-complete.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google