MiniSatの非決定変数の意味は何ですか？

Question

C++ライブラリとしてMiniSatを使用する場合、新しい変数はすべて、決定変数または非決定変数として作成できます。

私が大まかに理解しているところは、ソルバーが分岐の際に次にどの変数を使用するかを決めるときに、非決定変数は考慮されないということです。しかし、私のプロジェクトでは、式が実際にはUNSATだったにもかかわらず、ソルバーがSATを返したときに、非決定変数が含意の左側にあるときに同等の関係になるのではなく、問題に遭遇しました。

これは、非決定変数が2変数よりも長い式にある場合にのみ起こることを示しています（2変数式パスはソルバーに特殊なケースであるため、動作が異なります） 。

Answer 1

無決定変数の値は、推論によってのみ設定できます。 Minisatが使用する推論の唯一の方法はユニットルールです。したがって、すべての決定変数を設定しても、すべての非決定変数を設定するためにユニットルールが呼び出されない場合、後者の変数は決して設定されません。

非決定変数を持つ通常の理由は、決定変数の固定セットの設定が他のすべての変数の値を暗示するようにCNFインスタンスが構造化されていることです。

この例は、nビット整数の素因数を見つけるためのCNFインスタンスです。インスタンスは必ず乗算を実装するシフト加算回路のチェーンを実装しますが、乗算回路への入力である2（n-1）ビットを設定するだけで済みます。これらのビットを表す変数は決定変数になり、他のすべての変数は非決定変数として安全に宣言できます。