c++ - 頂点被覆問題を SAT と最適化で解くには?

Question

そのため、現在、SAT を使用して最小頂点カバーの問題を解決する作業を行っています。グラフ G = {V,E} のコード化には k 個の頂点カバーがあり、節は次のとおりです。

Let n = sizeof(V);

まず、少なくとも 1 つの頂点が頂点カバー内にあります。

For i in {1..k}
    Add clause (x<1,i> ∨ x<2,i> ∨ ··· ∨ x<n,i>);

次に、頂点カバーに 1 つの頂点が 2 回出現することはありません。

For j in {1..n}
    For l and m in {1..k} with l < m
        Add clause (¬x<j,l> ∨ ¬x<j,m>) 

その後、頂点カバーの特定の位置に 1 つの頂点のみが表示されます。

For j in {1..k}
    For l and m in {1..n} with l < m
        Add clause (¬x<l,j> ∨ ¬x<m,j>) 

最後に、頂点カバーの少なくとも 1 つの頂点がエッジから来る必要があります。

For i and j in each edge e from E
    Add clause (x<i,1> ∨ x<i,2> ∨ ... ∨ x<i,k> ∨ x<j,1> ∨ ... ∨ x<j,k>)

このエンコーディングを使用して最小限の頂点カバーを取得できるようになりましたが、効率はかなり悪いです。頂点が 20 未満のグラフの結果しか取得できません。それ以外の場合は、結果を取得するのに数分から数時間かかります。私は今、SAT からさらに、おそらく 3SAT まで減らすことを考えています。しかし、同じ結果を得るために、すべての節を nCNF から 3CNF に単純に変更することはできないようです。次に何をすべきかを理解するのを手伝ってくれる人はいますか？新しいエンコーディングが必要ですか?

どうもありがとう。

ところで、私はソルバーに MiniSAT を使用しています。