0

私の理解では、インクリメンタル SAT 解法は、互いに非常に近いさまざまなモデルを評価するのに役立ちます。

これを使用してモデルを評価し、後で変更した場合は、以前のソリューションを使用して再評価し、より迅速な結果を得たいと考えています。しかし、さまざまな SAT ソルバー (Sat4J、Minisat、mathsat5) を調べたところ、すべてのモデルが 1 回の実行で提示された場合にのみ、漸進的に解決できるようです。

私はSATの解決にかなり慣れていないので、何かを見落としているかもしれません。後で使用するために解決インスタンスを保存する方法はありませんか? インスタンスを閉じると、すべての学習が失われますか?

4

2 に答える 2

0

インクリメンタル モードでは、ソルバーに新しい制約を与えることができます。

設定に応じて、ソルバーは以前に学習した句とヒューリスティックを忘れる場合と忘れない場合があります。

インクリメンタル モードを十分に活用し、以前にシステムに入力された制約を破棄するには、「仮定」、つまりソルバーで制約を有効または無効にする特定の変数を使用する必要があります。

たとえば、ミニサット ニュースグループのこのディスカッションを参照してください: https://groups.google.com/forum/#!topic/minisat/ffXxBpqKh90

于 2016-05-25T08:09:37.590 に答える