david_putnam

Posted on | In

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
def DP(clauses, V):
    while True:
        change = False

        # check if the set of clause if empty
        if len(clauses) == 0:
            return V
        
        # check if empty clause in the set
        for i in clauses:
            if len(i) == 0:
                return False
            
        # check if there is a singleton clause in the set
        for i in clauses:
            if len(i) == 1:
                atom = i[0]
                clauses = propagate(clauses, atom)
                if '-' in atom:
                    V[int(negate(atom))] = False
                else:
                    V[int(atom)] = True
                change = True
                break
        
        # check if pure literal in the set
        pure_literal = ''
        for atom in V:
            if is_pure(clauses, atom):
                pure_literal = atom
                break
        if pure_literal != '':
            clauses = propagate(clauses, pure_literal)
            if '-' in pure_literal:
                V[int(negate(pure_literal))] = False
            else:
                V[int(pure_literal)] = True
            change = True
    
        if change is False:
            break
    
    # get the first unassigned atom
    for c in clauses:
        if len(c) != 0:
            first = c[0]
            break
        else:
            continue
    if '-' in first:
        first = negate(first)

    # set it to be True
    clauses_copy = copy.deepcopy(clauses)
    V[int(first)] = True
    clauses = propagate(clauses, first)
    result = DP(clauses, V)
    if result is not False:
        return result

    # set it to be False
    V[int(first)] = False
    clauses_copy = propagate(clauses_copy, negate(first))
    return DP(clauses_copy, V)