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
- 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 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.
def DP(clauses, V):