-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathresolutionAlgorithm.py
57 lines (44 loc) · 2.81 KB
/
resolutionAlgorithm.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
from clause import Clause
from generalLogicParser import convertToCNF
class Resolution:
def solve(self,kb,query):
cnfClausesList = []
for clause in kb:
cnfClausesList.append(convertToCNF(clause)) # convert the clauses to CNF and add them to a list
negationOfQuery = Clause(operator="~",right=query)
cnfClausesList.append(convertToCNF(negationOfQuery)) # convert the negation of query to CNF and add to the list
cnfClausesList = [str(clause).replace("(","").replace(")","") for clause in cnfClausesList] # remove all ()
clauses = []
for clause in cnfClausesList:
for disjunctionOfSymbol in clause.split("&"): # split the clause at &
clauses.append(disjunctionOfSymbol)
clauses = [clause.split("||") for clause in clauses] # split the clause at ||
clauses = {frozenset(clause) for clause in clauses} # By making clauses a set, we can remove the duplicate symbols
new = set()
while True:
clauseList = [list(clause) for clause in clauses] # convert the set back to List to use List operations
for i in range(len(clauseList)-1):
for j in range(i+1,len(clauseList)):
resolvents = []
canBeResolved = False
for literal in clauseList[i]:
if literal[0] != "~" and (("~"+ literal) in clauseList[j]): # check if there is a negation of the symbol in clauseList[j]
result = [symbol for symbol in clauseList[i] if symbol != literal]
result.extend([symbol for symbol in clauseList[j] if symbol != ("~" + literal)])
resolvents.append(result)
canBeResolved = True
elif literal[0] == "~" and literal[1:] in clauseList[j]:
result = [symbol for symbol in clauseList[i] if symbol != literal]
result.extend([symbol for symbol in clauseList[j] if symbol != literal[1:] ])
resolvents.append(result)
canBeResolved = True
if not canBeResolved:
resolvents.append(clauseList[i].copy())
resolvents.append(clauseList[j].copy())
if [] in resolvents: # return true if the list contain an empty list
return True
resolventsSet = {frozenset(clause) for clause in resolvents}
new = new.union(resolventsSet) # the union of new and resolventsSet
if new.issubset(clauses): # return false if there is no new clause has been resolved
return False
clauses = clauses.union(new)# the union of clauses and new