(充足可能な) (線形) 整数充足可能性問題があります。この問題には、とりわけ、ブーリアン値の変数が多数含まれており、それらを x 1 ...x nと呼びます。制約の 1 つは、sum(x 1 ...x n ) = C です。これらの変数の固定値と、これらの変数の固定値 (すべての可能なソリューションで、これらの変数のどれが特定の値 (0 または 1、これらはブール値であるため) を取るかなど)。
私は実用的な解決策を持っていますが、それはただ遅いです（穏やかに言えば）：
- x 1 == 0という制約を追加します
- 問題が解決可能かどうかを確認する
- 手順 1 で追加した制約を削除します。
- x 1 == 1という制約を追加します
- 問題が解決可能かどうかを確認する
- 手順 4 で追加した制約を削除します
- 2 と 5 の少なくとも 1 つが成功したことをアサートします。
- 両方が成功した場合、変数は固定されません。それ以外の場合、変数は、問題がまだ満足できる制約に固定されます。
- x 2 ...x nに対して 1...8 を繰り返す
これの問題は、遅いことです。特に、問題を O(n) 回、つまり 2*n 回解く必要があります。（ソルバーをウォームスタートするために以前のソリューションを渡していますが、ソルバーを開始するだけでほとんど時間がかかります。）
もっと速い方法はありますか？特に、ソルバーの呼び出し回数を減らす必要があるものは?
私が考えていたことは、残念ながらそのままでは機能しませんが、それを ILP 問題に変えて 2 回解決することです。同じものを最小化し、どの変数が変化するかをチェックします。残念ながら、これは一般的には機能しません。(カウンター) の例: ブール変数and 、 where . どちらの変数も固定されていなくても、最大化と最小化を行っても同じ結果が得られます。xyx+y=1