David Putnam algorithm

The David Putnam algorithm is aimed to check the validity of a first-order logic formula, which solves the SAT (boolean satisfiability problem). It is a recursion function, and it contains a while loop checks following things:

• It contains some clauses and it is not an empty set.
• There is no empty clause in the set.
• If there is a singleton clause in the set, set it to be true and propagate.
• If there is a pure literal (which means that the negation of it is not in the set), set it to be true and propagate.

The propagate function works as followed:

• Delete any clause that contraining literal P, which is set to be True.
• Delete ~P in any clause while keep the remaining unchanged.

The code block below show the algorithm in Python 3.