図に示すようなメッシュ ネットワークがあります。現在、この sat ネットワークのすべてのエッジに値を割り当てています。プログラムで、割り当てに閉じたループがないことを提案したいと思います。たとえば、左上の四角形の制約は次のように記述できます -
E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0であるため、ループを形成しないようにするには、どちらかのリンクを非アクティブにする必要があります。ただし、この種のネットワークでは、多くのループが発生する可能性があります。
たとえば、エッジによって形成されるループ - E0, E3, E7, E11, E15, E12, E5, E1。
ここでの問題は、このネットワークで発生する可能性のあるループの可能な組み合わせをそれぞれ説明する必要があることです。1つの可能な式で制約を書き込もうとしましたが、うまくいきませんでした。
この状況をエンコードする方法があれば、誰でもポインタを投げることができますか? 参考までに、私は Z3 Sat Solver を使用しています。
