boolean-logic - 布尔公式可满足性 - 将最小数量的变量设置为真求解

Question

我在想出伪代码来解决布尔可满足性问题时遇到了麻烦，使用最少数量的变量设置为真。

我有一个可满足的 number(H) 方法，我可以调用它来获取需要设置为 true 的变量的最小数量，以便布尔公式可以满足。

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;

}

这是我目前的逻辑。如果我走在正确的轨道上，请告诉我。