If a clause contains only a single unassigned literal you can only satisfy by assigning the value that yields this literal as true. Therefore it isn't necessary to make a choice in this case even though unitprop checks. You can avoid a considerable part of the search space by implementing this simple check.

Very clever otherwise!