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

1 | def DP(clauses, V): |