3 ms·
-- if formula is a null list, this clause will match: dpll (SolverState [] r) = return r -- otherwise this one will match: dpll (SolverState f r) =
by nandemo 15y ago
-- if formula is a null list, this clause will match:
dpll (SolverState [] r) = return r
-- otherwise this one will match:
dpll (SolverState f r) =
-- so it is never the case that null f is true here:
if null f then return r
And the second clause is basically the same as "dpll s =".
- gatlin 15y agoEmpirically I know this not to be the case. Take out the if statement and then run this: > solve [[1],[2]] You'll get "Nothing" when in fact the answer is [2,1]. The reason is that unitpropagate could potentially empty the list before chooseLiteral gets at it. However, I run unitpropagate first because it cuts down the search space dramatically.