-
Notifications
You must be signed in to change notification settings - Fork 1
/
dpll_solve.py
176 lines (138 loc) · 5.13 KB
/
dpll_solve.py
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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
import copy
def check_done(clauses):
""" Figures out if the problem is solved, not solvable, or unfinished.
inputs
clauses: 2D array of clauses
returns
True if all clauses are satisfied
False if there's a clause that cannot be satisfied
None if there are still undetermined clauses left
"""
if(len(clauses) == 0):
return True
for c in clauses:
if(len(c) == 0):
return False
return None
def assign(assm, p):
""" Assigns the literal 'p' to a value in the dictionary 'assm'. If the input is
negated, assigns p to false. If the input is not negated, assigns p to true.
inputs
assm: dictionary of literal assignments
p: a literal represented by an integer value
"""
if p >= 0:
assm[abs(p)] = 1
else:
assm[abs(p)] = 0
def simplify(clauses, p):
""" Updates clauses to reflect the impact of the assignment of literal 'p'.
If clauses are now satisfied by p, they can be removed. If clauses are not
satisfied by p, then p is no longer relevant and is removed from the clause.
inputs
clauses: 2D array of clauses
p: a literal represented by an integer value
returns
copy_clauses: 2D array of clauses, updated to remove references to literal 'p'
"""
copy_clauses = copy.deepcopy(clauses)
i = 0
while i < len(copy_clauses):
# get rid of clauses that are now satisfied by true
if p in copy_clauses[i]:
del copy_clauses[i]
# get rid of references to this bc it's unhelpful as false
else:
if -p in copy_clauses[i]:
copy_clauses[i].remove(-p)
i += 1
return copy_clauses
def solve_sat(clauses, assm):
""" Recursively solves the rest of the satisfiability problem. Base case:
we have determined satisfiability using check_done(). Otherwise, pick
a literal that hasn't been assigned yet, try assigning it to false then
recurse. If that doesn't work, try assigning it to true then recurse.
inputs
clauses: 2D array of clauses
assm: dictionary of literal assignments
returns
sat: boolean that is true if satisfiable, false otherwise
assm: dictionary of literals to satisfying assignments
"""
result = check_done(clauses)
if result != None:
return result, assm
copy_assm = copy.deepcopy(assm)
val_list = list(copy_assm.values())
key_list = list(copy_assm.keys())
idx = val_list.index(None)
p = key_list[idx]
# try false first
assign(copy_assm, -p)
copy_clauses = simplify(clauses, -p)
result = solve_sat(copy_clauses, copy_assm)
if(result[0]): return result
# if that didn't work, try true
assign(copy_assm, p)
copy_clauses = simplify(clauses, p)
return solve_sat(copy_clauses, copy_assm)
def get_vars(clauses):
""" Picks out all of the literals from the clauses to create
the assignments dictionary.
inputs
clauses: 2D array of clauses
returns
assm: dictionary meant to hold the assignments of the literals
"""
assm = dict()
for c in clauses:
for p in c:
assm[abs(p)] = None
return assm
def assign_pure_literals(clauses, assm):
""" Assigns pure literals - literals that show up in a lenth-1 clause
and therefore have an obvious and necessary assignment value.
inputs
clauses: 2D array of clauses
assm: dictionary of literal assignments
returns
clauses: 2D array of clauses updated to remove references to pure literals
assm: dictionary of updated literal assignments
"""
i = 0
while i < len(clauses):
if(len(clauses[i]) == 1):
assign(assm, clauses[i][0])
clauses = simplify(clauses, clauses[i][0])
i = 0
else:
i += 1
return clauses, assm
def dpll(clauses):
""" Solves the satisfiability problem. First checks whether satisfiability
has been determined using check_done(). Otherwise, it sets up the variable
assignment dictionary, assigns pure literals, and runs the solver.
inputs
clauses: 2D array of clauses
returns
sat: boolean that is true if satisfiable, false otherwise
assm: dictionary of literals to satisfying assignments
"""
# see if the problem is already solved
result = check_done(clauses)
if result != None: return result
assm = get_vars(clauses)
# assign the variables that can only go one way
clauses, assm = assign_pure_literals(clauses, assm)
# solve the rest of the unit clauses recursively
return solve_sat(clauses, assm)
# DO NOT USE 0 AS A LITERAL AS IT CANNOT HOLD A SIGN VALUE
# Small test cases provided below
# TRUE
# clauses = [[1, -5, 4, 2], [-1, 5, 3, 4, 2], [-3, -4, 2], [3], [5]]
# FALSE
# clauses = [[3, 1, 2], [3, 1, -2], [3, -1, 2], [-3, 1, 2],
# [3, -1, -2], [-3, 1, -2], [-3, -1, 2], [-3, -1, -2]]
# TRUE
# clauses = [[3, 1, -2], [-3, -1, 2], [-3, 1, -2]]
# print(dpll(clauses))