4

Composite Specification Pattern の LINQ ベースの実装は多数あります。Subsumption を使用したものは見たことがありません。

文書化されている (ブログなど) か、オープン ソースとして公開されている例はありますか? ExpressionVisitor ですべての仕様を正規の論理形式 (CNF/DNF) に変換することで、これがどのように機能するかについてのアイデアと概念実証がありますが、これが過度に複雑であることが懸念されます。より良い方法はありますか？

4

1 に答える 1

2

これが非常に複雑になるのではないかと心配しています。もっと良い方法はありますか？

簡単な答えは「いいえ、ありません」です1

長い答え：「過度に複雑」は問題の本質を捉えています。それはNP困難です。これは、充足可能性問題がNP完全であるという事実に依存する短い非公式の証明です。

  • 2つのブール式がAあり、B
  • Aを意味するかどうかB、または同等に、およびが依存する¬A | B変数のすべての割り当てについてテストする必要があります。言い換えれば、トートロジーである証拠が必要です。ABF = ¬A | B
  • トートロジーテストを多項式時間で実行できると仮定します
  • を考え¬FてみましょうF。トートロジーでない場合にのみF充足可能¬F
  • 架空の多項式アルゴリズムを使用し¬Fて、トートロジーであることをテストします
  • 「F充足可能」に対する答えは¬F、「トートロジーである」に対する答えの逆です。
  • したがって、多項式トートロジーチェッカーの存在は、充足可能性問題がにあることを意味しPますP=NP。

もちろん、問題がNP困難であるという事実は、実際のケースの解決策がないことを意味するわけではありません。実際、標準形に変換するアプローチでは、多くの現実の状況でOKの結果が得られる可能性があります。ただし、既知の「優れた」アルゴリズムがないため、実用的なソリューションの積極的な開発が妨げられることがよくあります2。

1「ただしP=NP」の免責事項が義務付けられています。

2「合理的に良い」解決策がうまくいかない限り、「偽陰性」を許容すれば、問題の場合に非常によく当てはまる可能性があります。

于 2012-12-11T20:12:16.087 に答える