I am writing a SAT solver and I started implementing a DPLL algorithm. I understand the algorithm and how it works, I also implemented a variation of it, but what bothers me is the next thing.
function DPLL(Φ)
if Φ is a consistent set of literals
then return true;
if Φ contains an empty clause
then return false;
for every unit clause l in Φ
Φ ← unit-propagate(l, Φ);
for every literal l that occurs pure in Φ
Φ ← pure-literal-assign(l, Φ);
l ← choose-literal(Φ);
return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));
What does it mean, that Φ is a consistent set of literals? I understand that inconsistent implies false, meaning that consistent implies not false. So why can we return true if the current assignment doesn't falsify the problem?
The way I implemented my SAT solver is, that whenever it comes across the assignment that made all clauses true, I returned that assignment and the algorithm was done. But since for given assignment, all clauses must be true in order for it to be a solution to the problem, I don't understand, how can one return true in case that an assignment just satisfies the problem (I assume I am getting something wrong here, but since if Φ is consistent, then it means it is not false, but it can still be undecidable?).
Φ is a consistent set of literals when it contains only literals and a literal and its negation does not appear in Φ. The DPLL algorithm, through the pure and unit rules, gradually converts the list of clauses into a list of literals that satisfy all the original clauses. The algorithm is done when that happens (Φ is a consistent set of literals) or when it runs out of literal assignments to try and the topmost DPLL call returns false.