Empirically 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,

Empirically 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.