does the pseudocode keep looping?

[U Albert]

I'm trying to follow the pseudocode, and it found that ex3.cnf was indeed
UNSAT. The SAT ones, however, are problematic. After a bit of
checking, I've found that the program does find a vector that works, but solve and
branch just keep calling each other, incrementing the dlevel as they go.
Also, getNextVar starts returning 0 after a while. I feel like adding
stuff to the pseudocode, but it looks good to me as is. Anyone have
advice for this?

[Alexander Smith]

In solve(), if you run out of unassigned variables, then you should return
SAT. getNextVar() is returning 0 to tell you that there are no more
unassigned variables. (Look at comment at the top of getNextVar() in
solve_given.c.) So, in solve(), after calling getNextVar() you should
check its return value. If there are no more unassigned variables, then it
means you have assigned a value to every variable in the formula, and
therefore you have found a satisfying assignment.

Alexander

Post by U Albert
I'm trying to follow the pseudocode, and it found that ex3.cnf was indeed
UNSAT. The SAT ones, however, are problematic. After a bit of
checking, I've found that the program does find a vector that works, but solve and
branch just keep calling each other, incrementing the dlevel as they go.
Also, getNextVar starts returning 0 after a while. I feel like adding
stuff to the pseudocode, but it looks good to me as is. Anyone have
advice for this?