boolean-logic - ブール式の充足可能性 - 変数の最小量を True に設定して解く

Question

true に設定された最小量の変数を使用してブール充足可能性問題を解決するための疑似コードを考え出すのに問題があります。

ブール式を満足できるものにするために true に設定する必要がある変数の最小数を取得するために呼び出すことができるメソッド satisfiable number(H) があります。

find-sat-min(f) {
if (not SAT(f)) return 0

L = {x | x is variable in f};
S = {};
int trueCount = 0;

for (x in L) {
    if (SAT(f ^ x) && trueCount < satisfiable number(f)) {
        S = S U {x};
        f = f ^ x;
        trueCount++;
    }
    else {
        S = S U {NOT x};
        f = f ^ NOT x;
    }
}

return S;

}

これが私の現在のロジックです。私が正しい軌道に乗っているかどうか教えてください。