Удовлетворенность булевой формулы - решение с минимальным количеством переменных, установленным в True

Question

У меня возникли проблемы с созданием псевдокода для решения проблемы булевой выполнимости с использованием минимального количества переменных, установленного в значение true.

У меня есть метод выполнимого числа (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;

}

Вот моя текущая логика. Пожалуйста, дайте мне знать, если я на правильном пути.