-
Notifications
You must be signed in to change notification settings - Fork 0
/
dpllAlgorithm.py
62 lines (48 loc) · 2.44 KB
/
dpllAlgorithm.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
from clause import Clause
from generalLogicParser import convertToCNF
import random
class DPLLAlgorithm:
def solve(self,kb,query):
cnfClausesList = []
for clause in kb:
cnfClausesList.append(convertToCNF(clause)) # convert clause to cnf
negationOfQuery = Clause(operator="~",right=query)
cnfClausesList.append(convertToCNF(negationOfQuery)) # convert negation of query to CNF
cnfClausesList = [str(clause).replace("(","").replace(")","") for clause in cnfClausesList]
clauses = []
for clause in cnfClausesList:
for disjunctionOfSymbol in clause.split("&"):
clauses.append(disjunctionOfSymbol)
clauses = [clause.split("||") for clause in clauses]
clauses = {frozenset(clause) for clause in clauses} # By making clauses a set, we can remove the duplicate symbols
return not self.dpll(clauses)
def dpll(self,formula):
if formula == set(): # return true if formula has no clause
return True
if frozenset() in formula: # return false if formula has an empty clause
return False
for clause in formula:
if len(clause) == 1: # check if there is an unit clause in formula
return self.dpll(self.simplify(formula,list(clause)[0]))
literal = random.choice(random.choice([list(clause) for clause in formula])) # choose a random literal in the formula
if self.dpll(self.simplify(formula,literal)):
return True
else:
if literal[0] == "~":
negationLiteral = literal[1:]
else:
negationLiteral = "~" + literal
return self.dpll(self.simplify(formula,negationLiteral))
def simplify(self,formula,literal):
newFormula = set()
for clause in formula:
if literal in clause:
continue # remove clauses that contains the literal
# remove the negation of literal in the clauses
if literal[0] != "~" and "~" + literal in clause:
newFormula.add(frozenset({subClause for subClause in clause if subClause != ("~" + literal)}))
elif literal[0] == "~" and literal[1:] in clause:
newFormula.add(frozenset({subClause for subClause in clause if subClause != literal[1:]}))
else:
newFormula.add(frozenset({subClause for subClause in clause}))
return newFormula