CODEWITHSUNDEEP
boolean-logicsatisfiability
BostonMan
BostonMan

Reputation: 161

Boolean Formula Satisfiability - Solving with Minimum Amount of Variables Set to True

I am having trouble coming up with the pseudocode to solve the Boolean satisfiability problem using the minimum amount of variables set to true.

I have a method satisfiable number(H) that I can call to obtain the minimum number of variables needed to be set to true in order for the Boolean formula to be satisfiable. 

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;

}

Here's my current logic. Please let me know if I'm on the right track.

Upvotes: 0

Views: 393

Answers (0)

Related Questions