カスタマイズされた集合被覆問題からsatに変換しているので、問題にsatソルバーを使用できる可能性があります。
私の問題は次のとおりです。sat問題の用語で相互作用する変数のセットがいくつかあります。の線に沿った何かx_i v x_j v x_k; y_i v y_j v y_k。
しかし、私が正しく理解できないように見えるのは、変数の両方のセットが組み合わせとして同じ占有率を持ってはならないということです。たとえば、X_iと等しくすることができますx_jが、セット全体を均等に占有してはなりません。
充足可能性ソルバーで使用できるように、それをどのように表現しますか？