From dde46111f9d1048364039ffd8235b076c00cfa8e Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Fri, 6 Nov 2020 16:58:32 +0530 Subject: [PATCH 1/8] DPLL algorithm --- other/dpll.py | 314 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 314 insertions(+) create mode 100644 other/dpll.py diff --git a/other/dpll.py b/other/dpll.py new file mode 100644 index 000000000000..8a530a19e53f --- /dev/null +++ b/other/dpll.py @@ -0,0 +1,314 @@ +""" +Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm +for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. + +For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm +""" + +import random + + +class Clause(): + """ + A clause represented in CNF. + A clause is a set of literals, either complemented or otherwise. + For example: + {A1, A2, A3'} is the clause (A1 v A2 v A3') + {A5', A2', A1} is the clause (A5' v A2' v A1) + """ + + def __init__(self, no_of_literals, literals): + """ + Represent the number of literals, the literals themselves, and an assignment in a clause." + """ + self.no_of_literals = no_of_literals + self.literals = [l for l in literals] + self.literal_values = dict() + for l in self.literals: + self.literal_values[l] = None # Assign all literals to None initially + + def __str__(self): + """ + To print a clause as in CNF. + Variable clause holds the string representation. + """ + clause = "{ " + for i in range(0, self.no_of_literals): + clause += (self.literals[i] + " ") + if i != self.no_of_literals - 1: + clause += ", " + clause += "}" + + return clause + + def assign(self, model): + """ + Assign values to literals of the clause as given by model. + """ + i = 0 + while i < self.no_of_literals: + symbol = self.literals[i][:2] + if symbol in model.keys(): + val = model[symbol] + else: + i += 1 + continue + if val != None: + if self.literals[i][-1] == "'": + val = not val #Complement assignment if literal is in complemented form + self.literal_values[self.literals[i]] = val + i += 1 + + def evaluate(self, model): + """ + Evaluates the clause till the extent possible with the current assignments in model. + This has the following steps: + 1. Return True if both a literal and its complement exist in the clause. + 2. Return True if a single literal has the assignment True. + 3. Return None(unable to complete evaluation) if a literal has no assignment. + 4. Compute disjunction of all values assigned in clause. + """ + for l in self.literals: + if len(l) == 2: + symbol = l + "'" + if symbol in self.literals: + return True + else: + symbol = l[:2] + if symbol in self.literals: + return True + + self.assign(model) + result = False + for j in self.literal_values.values(): + if j == True: + return True + elif j == None: + return None + for j in self.literal_values.values(): + result = result or j + return result + +class Formula(): + """ + A formula represented in CNF. + A formula is a set of clauses. + For example, + {{A1, A2, A3'}, {A5', A2', A1}} is the formula ((A1 v A2 v A3') and (A5' v A2' v A1)) + """ + def __init__(self, no_of_clauses, clauses): + """ + Represent the number of clauses and the clauses themselves. + """ + self.no_of_clauses = no_of_clauses + self.clauses = [c for c in clauses] + + def __str__(self): + """ + To print a formula as in CNF. + Variable formula holds the string representation. + """ + formula = "{ " + for i in range(0, self.no_of_clauses): + formula += (str(self.clauses[i]) + " ") + if i != self.no_of_clauses - 1: + formula += ", " + formula += "}" + + return formula + +def generate_clause(): + """ + Randomly generate a clause. + All literals have the name Ax, where x is an integer from 1 to 5. + """ + literals = [] + no_of_literals = random.randint(1, 5) + base_var = "A" + i = 0 + while i < no_of_literals: + var_no = random.randint(1, 5) + var_name = base_var+str(var_no) + var_complement = random.randint(0, 1) + if var_complement == 1: + var_name += "'" + if var_name in literals: + i -= 1 + else: + literals.append(var_name) + i+=1 + clause = Clause(no_of_literals, literals) + return clause + +def generate_formula(): + """ + Randomly generate a formula. + """ + clauses = [] + no_of_clauses = random.randint(1, 10) + i = 0 + while i < no_of_clauses: + clause = generate_clause() + if clause in clauses: + i -= 1 + else: + clauses.append(clause) + i += 1 + formula = Formula(no_of_clauses, clauses) + return formula + +def generate_parameters(formula): + """ + Return the clauses and symbols from a formula. + A symbol is the uncomplemented form of a literal. + For example, + Symbol of A3 is A3. + Symbol of A5' is A5. + + """ + clauses = formula.clauses + symbols_set = [] + for clause in formula.clauses: + for literal in clause.literals: + symbol = literal[:2] + if symbol not in symbols_set: + symbols_set.append(symbol) + return clauses, symbols_set + +def find_pure_symbols(clauses, symbols, model): + """ + Return pure symbols and their assignments to satisfy the clause, if figurable. + Pure symbols are symbols in a formula that exist only in one form, either complemented or otherwise. + For example, + { { A4 , A3 , A5' , A1 , A3' } , { A4 } , { A3 } } has the pure symbols A4, A5' and A1. + This has the following steps: + 1. Ignore clauses that have already evaluated to be True. + 2. Find symbols that occur only in one form in the rest of the clauses. + 3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively. + """ + pure_symbols = [] + assignment = dict() + literals = [] + + for clause in clauses: + if clause.evaluate(model) == True: + continue + for l in clause.literals: + literals.append(l) + + for s in symbols: + sym = (s + "'") + if (s in literals and sym not in literals) or (s not in literals and sym in literals): + pure_symbols.append(s) + for p in pure_symbols: + assignment[p] = None + for s in pure_symbols: + sym = (s + "'") + if s in literals: + assignment[s] = True + elif sym in literals: + assignment[s] = False + return pure_symbols, assignment + +def find_unit_clauses(clauses, model): + """ + Returns the unit symbols and their assignments to satisfy the clause, if figurable. + Unit symbols are symbols in a formula that are: + - Either the only symbol in a clause + - Or all other literals in that clause have been assigned False + This has the following steps: + 1. Find symbols that are the only occurences in a clause. + 2. Find symbols in a clause where all other literals are assigned to be False. + 3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively. + """ + unit_symbols = [] + for clause in clauses: + if clause.no_of_literals == 1: + unit_symbols.append(clause.literals[0]) + else: + Fcount, Ncount = 0, 0 + for l,v in clause.literal_values.items(): + if v == False: + Fcount += 1 + elif v == None: + sym = l + Ncount += 1 + if Fcount == clause.no_of_literals - 1 and Ncount == 1: + unit.append(sym) + assignment = dict() + for i in unit_symbols: + symbol = i[:2] + if len(i) == 2: + assignment[symbol] = True + else: + assignment[symbol] = False + unit_symbols = [i[:2] for i in unit_symbols] + + return unit_symbols, assignment + +def DPLL(clauses, symbols, model): + """ + Returns the model if the formula is satisfiable, else None + This has the following steps: + 1. If every clause in clauses is True, return True. + 2. If some clause in clauses is False, return False. + 3. Find pure symbols. + 4. Find unit symbols. + """ + check_clause_all_true = True + for clause in clauses: + clause_check = clause.evaluate(model) + if clause_check == False: + return False, None + elif clause_check == None: + check_clause_all_true = False + continue + + if check_clause_all_true: + return True, model + + pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) + P = None + if len(pure_symbols) > 0: + P, value = pure_symbols[0], assignment[pure_symbols[0]] + + if P: + tmp_model = model + tmp_model[P] = value + tmp_symbols = [i for i in symbols] + if P in tmp_symbols: + tmp_symbols.remove(P) + return DPLL(clauses, tmp_symbols, tmp_model) + + unit_symbols, assignment = find_unit_clauses(clauses, model) + P = None + if len(unit_symbols) > 0: + P, value = unit_symbols[0], assignment[unit_symbols[0]] + if P: + tmp_model = model + tmp_model[P]=value + tmp_symbols = [i for i in symbols] + if P in tmp_symbols: + tmp_symbols.remove(P) + return DPLL(clauses, tmp_symbols, tmp_model) + P = symbols[0] + rest = symbols[1:] + tmp1, tmp2 = model, model + tmp1[P], tmp2[P] = True, False + + return DPLL(clauses, rest, tmp1) or DPLL(clauses, rest, tmp2) + +if __name__ == "__main__": + #import doctest + #doctest.testmod() + formula = generate_formula() + print(formula) + + clauses, symbols = generate_parameters(formula) + + solution, model = DPLL(clauses, symbols, {}) + + if solution: + print(model) + else: + print("Not satisfiable") \ No newline at end of file From be92721cc26ddd74379e6505f917f733c53442c5 Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Sat, 7 Nov 2020 17:58:24 +0530 Subject: [PATCH 2/8] Corrections complete --- other/dpll.py | 135 +++++++++++++++++++++++++++++++++++++------------- 1 file changed, 100 insertions(+), 35 deletions(-) diff --git a/other/dpll.py b/other/dpll.py index 8a530a19e53f..ac5945061d26 100644 --- a/other/dpll.py +++ b/other/dpll.py @@ -14,18 +14,26 @@ class Clause(): A clause is a set of literals, either complemented or otherwise. For example: {A1, A2, A3'} is the clause (A1 v A2 v A3') - {A5', A2', A1} is the clause (A5' v A2' v A1) + {A5', A2', A1} is the clause (A5' v A2' v A1) + + Create a set of literals and a clause with them + >>> literals = ["A1", "A2'", "A3"] + >>> clause = Clause(literals) + >>> print(clause) + { A1 , A2' , A3 } + + Create model + >>> model = {"A1": True} + >>> clause.evaluate(model) + True """ - def __init__(self, no_of_literals, literals): + def __init__(self, literals): """ - Represent the number of literals, the literals themselves, and an assignment in a clause." + Represent the literals and an assignment in a clause." """ - self.no_of_literals = no_of_literals - self.literals = [l for l in literals] - self.literal_values = dict() - for l in self.literals: - self.literal_values[l] = None # Assign all literals to None initially + self.literals = {literal : None for literal in literals} # Assign all literals to None initially + self.no_of_literals = len(self.literals) def __str__(self): """ @@ -34,7 +42,7 @@ def __str__(self): """ clause = "{ " for i in range(0, self.no_of_literals): - clause += (self.literals[i] + " ") + clause += str(list(self.literals.keys())[i]) + " " if i != self.no_of_literals - 1: clause += ", " clause += "}" @@ -47,16 +55,16 @@ def assign(self, model): """ i = 0 while i < self.no_of_literals: - symbol = self.literals[i][:2] + symbol = list(self.literals.keys())[i][:2] if symbol in model.keys(): val = model[symbol] else: i += 1 continue if val != None: - if self.literals[i][-1] == "'": + if list(self.literals.keys())[i][-1] == "'": val = not val #Complement assignment if literal is in complemented form - self.literal_values[self.literals[i]] = val + self.literals[list(self.literals.keys())[i]] = val i += 1 def evaluate(self, model): @@ -68,24 +76,24 @@ def evaluate(self, model): 3. Return None(unable to complete evaluation) if a literal has no assignment. 4. Compute disjunction of all values assigned in clause. """ - for l in self.literals: + for l in list(self.literals.keys()): if len(l) == 2: symbol = l + "'" - if symbol in self.literals: + if symbol in list(self.literals.keys()): return True else: symbol = l[:2] - if symbol in self.literals: + if symbol in list(self.literals.keys()): return True self.assign(model) result = False - for j in self.literal_values.values(): + for j in self.literals.values(): if j == True: return True elif j == None: return None - for j in self.literal_values.values(): + for j in self.literals.values(): result = result or j return result @@ -95,13 +103,21 @@ class Formula(): A formula is a set of clauses. For example, {{A1, A2, A3'}, {A5', A2', A1}} is the formula ((A1 v A2 v A3') and (A5' v A2' v A1)) + + Create two clauses and a formula with them + >>> c1 = Clause(["A1", "A2'", "A3"]) + >>> c2 = Clause(["A5'", "A2'", "A1"]) + + >>> f = Formula([c1, c2]) + >>> print(f) + { { A1 , A2' , A3 } , { A5' , A2' , A1 } } """ - def __init__(self, no_of_clauses, clauses): + def __init__(self, clauses): """ Represent the number of clauses and the clauses themselves. """ - self.no_of_clauses = no_of_clauses self.clauses = [c for c in clauses] + self.no_of_clauses = len(self.clauses) def __str__(self): """ @@ -137,7 +153,7 @@ def generate_clause(): else: literals.append(var_name) i+=1 - clause = Clause(no_of_literals, literals) + clause = Clause(literals) return clause def generate_formula(): @@ -154,7 +170,7 @@ def generate_formula(): else: clauses.append(clause) i += 1 - formula = Formula(no_of_clauses, clauses) + formula = Formula(set(clauses)) return formula def generate_parameters(formula): @@ -165,11 +181,21 @@ def generate_parameters(formula): Symbol of A3 is A3. Symbol of A5' is A5. + >>> c1 = Clause(["A1", "A2'", "A3"]) + >>> c2 = Clause(["A5'", "A2'", "A1"]) + + >>> f = Formula([c1, c2]) + >>> c, s = generate_parameters(f) + >>> l = [str(i) for i in c] + >>> print(l) + ["{ A1 , A2' , A3 }", "{ A5' , A2' , A1 }"] + >>> print(s) + ['A1', 'A2', 'A3', 'A5'] """ clauses = formula.clauses symbols_set = [] for clause in formula.clauses: - for literal in clause.literals: + for literal in clause.literals.keys(): symbol = literal[:2] if symbol not in symbols_set: symbols_set.append(symbol) @@ -185,6 +211,17 @@ def find_pure_symbols(clauses, symbols, model): 1. Ignore clauses that have already evaluated to be True. 2. Find symbols that occur only in one form in the rest of the clauses. 3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively. + + >>> c1 = Clause(["A1", "A2'", "A3"]) + >>> c2 = Clause(["A5'", "A2'", "A1"]) + + >>> f = Formula([c1, c2]) + >>> c, s = generate_parameters(f) + + >>> model = {} + >>> p, v = find_pure_symbols(c, s, model) + >>> print(p, v) + ['A1', 'A2', 'A3', 'A5'] {'A1': True, 'A2': False, 'A3': True, 'A5': False} """ pure_symbols = [] assignment = dict() @@ -193,7 +230,7 @@ def find_pure_symbols(clauses, symbols, model): for clause in clauses: if clause.evaluate(model) == True: continue - for l in clause.literals: + for l in clause.literals.keys(): literals.append(l) for s in symbols: @@ -220,21 +257,34 @@ def find_unit_clauses(clauses, model): 1. Find symbols that are the only occurences in a clause. 2. Find symbols in a clause where all other literals are assigned to be False. 3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively. + + >>> c1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) + >>> c2 = Clause(["A4"]) + >>> c3 = Clause(["A3"]) + + >>> f = Formula([c1, c2, c3]) + >>> c, s = generate_parameters(f) + + >>> model = {} + >>> u, v = find_unit_clauses(c, model) + + >>> print(u, v) + ['A4', 'A3'] {'A4': True, 'A3': True} """ unit_symbols = [] for clause in clauses: if clause.no_of_literals == 1: - unit_symbols.append(clause.literals[0]) + unit_symbols.append(list(clause.literals.keys())[0]) else: Fcount, Ncount = 0, 0 - for l,v in clause.literal_values.items(): + for l,v in clause.literals.items(): if v == False: Fcount += 1 elif v == None: sym = l Ncount += 1 if Fcount == clause.no_of_literals - 1 and Ncount == 1: - unit.append(sym) + unit_symbols.append(sym) assignment = dict() for i in unit_symbols: symbol = i[:2] @@ -246,7 +296,7 @@ def find_unit_clauses(clauses, model): return unit_symbols, assignment -def DPLL(clauses, symbols, model): +def dpll_algorithm(clauses, symbols, model): """ Returns the model if the formula is satisfiable, else None This has the following steps: @@ -254,6 +304,19 @@ def DPLL(clauses, symbols, model): 2. If some clause in clauses is False, return False. 3. Find pure symbols. 4. Find unit symbols. + + >>> c1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) + >>> c2 = Clause(["A4"]) + >>> c3 = Clause(["A3"]) + + >>> f = Formula([c1, c2, c3]) + >>> c, s = generate_parameters(f) + + >>> model = {} + >>> soln, model = dpll_algorithm(c, s, model) + + >>> print(soln, model) + True {'A4': True, 'A3': True} """ check_clause_all_true = True for clause in clauses: @@ -278,7 +341,7 @@ def DPLL(clauses, symbols, model): tmp_symbols = [i for i in symbols] if P in tmp_symbols: tmp_symbols.remove(P) - return DPLL(clauses, tmp_symbols, tmp_model) + return dpll_algorithm(clauses, tmp_symbols, tmp_model) unit_symbols, assignment = find_unit_clauses(clauses, model) P = None @@ -290,25 +353,27 @@ def DPLL(clauses, symbols, model): tmp_symbols = [i for i in symbols] if P in tmp_symbols: tmp_symbols.remove(P) - return DPLL(clauses, tmp_symbols, tmp_model) + return dpll_algorithm(clauses, tmp_symbols, tmp_model) P = symbols[0] rest = symbols[1:] tmp1, tmp2 = model, model tmp1[P], tmp2[P] = True, False - return DPLL(clauses, rest, tmp1) or DPLL(clauses, rest, tmp2) + return dpll_algorithm(clauses, rest, tmp1) or dpll_algorithm(clauses, rest, tmp2) if __name__ == "__main__": - #import doctest - #doctest.testmod() + import doctest + doctest.testmod() + formula = generate_formula() - print(formula) + print(f'The formula {formula} is', end = " ") clauses, symbols = generate_parameters(formula) - solution, model = DPLL(clauses, symbols, {}) + solution, model = dpll_algorithm(clauses, symbols, {}) if solution: + print(" satisfiable with the assignment: ") print(model) else: - print("Not satisfiable") \ No newline at end of file + print(" not satisfiable") From 17e70198d9f47000c886a1b44a36555915f00a7e Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Sat, 7 Nov 2020 18:19:09 +0530 Subject: [PATCH 3/8] Formatting --- other/dpll.py | 155 ++++++++++++++++++++++++++++---------------------- 1 file changed, 88 insertions(+), 67 deletions(-) diff --git a/other/dpll.py b/other/dpll.py index ac5945061d26..b971531c2748 100644 --- a/other/dpll.py +++ b/other/dpll.py @@ -1,14 +1,17 @@ """ -Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm -for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. +Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, +backtracking-based search algorithm for deciding the satisfiability of +propositional logic formulae in conjunctive normal form, +i.e, for solving the CNF-SAT problem. -For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm +For more information about the algorithm: +https://en.wikipedia.org/wiki/DPLL_algorithm """ import random -class Clause(): +class Clause: """ A clause represented in CNF. A clause is a set of literals, either complemented or otherwise. @@ -17,7 +20,7 @@ class Clause(): {A5', A2', A1} is the clause (A5' v A2' v A1) Create a set of literals and a clause with them - >>> literals = ["A1", "A2'", "A3"] + >>> literals = ["A1", "A2'", "A3"] >>> clause = Clause(literals) >>> print(clause) { A1 , A2' , A3 } @@ -32,13 +35,14 @@ def __init__(self, literals): """ Represent the literals and an assignment in a clause." """ - self.literals = {literal : None for literal in literals} # Assign all literals to None initially + # Assign all literals to None initially + self.literals = {literal: None for literal in literals} self.no_of_literals = len(self.literals) - + def __str__(self): """ - To print a clause as in CNF. - Variable clause holds the string representation. + To print a clause as in CNF. + Variable clause holds the string representation. """ clause = "{ " for i in range(0, self.no_of_literals): @@ -46,9 +50,9 @@ def __str__(self): if i != self.no_of_literals - 1: clause += ", " clause += "}" - + return clause - + def assign(self, model): """ Assign values to literals of the clause as given by model. @@ -59,51 +63,53 @@ def assign(self, model): if symbol in model.keys(): val = model[symbol] else: - i += 1 - continue - if val != None: + i += 1 + continue + if val is not None: + # Complement assignment if literal is in complemented form if list(self.literals.keys())[i][-1] == "'": - val = not val #Complement assignment if literal is in complemented form + val = not val self.literals[list(self.literals.keys())[i]] = val i += 1 - + def evaluate(self, model): """ - Evaluates the clause till the extent possible with the current assignments in model. + Evaluates the clause with the assignments in model. This has the following steps: 1. Return True if both a literal and its complement exist in the clause. 2. Return True if a single literal has the assignment True. 3. Return None(unable to complete evaluation) if a literal has no assignment. 4. Compute disjunction of all values assigned in clause. """ - for l in list(self.literals.keys()): - if len(l) == 2: - symbol = l + "'" + for literal in list(self.literals.keys()): + if len(literal) == 2: + symbol = literal + "'" if symbol in list(self.literals.keys()): return True else: - symbol = l[:2] + symbol = literal[:2] if symbol in list(self.literals.keys()): - return True + return True self.assign(model) result = False for j in self.literals.values(): - if j == True: + if j is True: return True - elif j == None: + elif j is None: return None for j in self.literals.values(): result = result or j return result -class Formula(): + +class Formula: """ A formula represented in CNF. A formula is a set of clauses. For example, - {{A1, A2, A3'}, {A5', A2', A1}} is the formula ((A1 v A2 v A3') and (A5' v A2' v A1)) - + {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1)) + Create two clauses and a formula with them >>> c1 = Clause(["A1", "A2'", "A3"]) >>> c2 = Clause(["A5'", "A2'", "A1"]) @@ -112,27 +118,29 @@ class Formula(): >>> print(f) { { A1 , A2' , A3 } , { A5' , A2' , A1 } } """ + def __init__(self, clauses): """ Represent the number of clauses and the clauses themselves. """ self.clauses = [c for c in clauses] self.no_of_clauses = len(self.clauses) - + def __str__(self): """ - To print a formula as in CNF. - Variable formula holds the string representation. + To print a formula as in CNF. + Variable formula holds the string representation. """ formula = "{ " for i in range(0, self.no_of_clauses): - formula += (str(self.clauses[i]) + " ") + formula += str(self.clauses[i]) + " " if i != self.no_of_clauses - 1: formula += ", " formula += "}" - + return formula + def generate_clause(): """ Randomly generate a clause. @@ -144,7 +152,7 @@ def generate_clause(): i = 0 while i < no_of_literals: var_no = random.randint(1, 5) - var_name = base_var+str(var_no) + var_name = base_var + str(var_no) var_complement = random.randint(0, 1) if var_complement == 1: var_name += "'" @@ -152,10 +160,11 @@ def generate_clause(): i -= 1 else: literals.append(var_name) - i+=1 + i += 1 clause = Clause(literals) return clause + def generate_formula(): """ Randomly generate a formula. @@ -173,6 +182,7 @@ def generate_formula(): formula = Formula(set(clauses)) return formula + def generate_parameters(formula): """ Return the clauses and symbols from a formula. @@ -198,26 +208,30 @@ def generate_parameters(formula): for literal in clause.literals.keys(): symbol = literal[:2] if symbol not in symbols_set: - symbols_set.append(symbol) + symbols_set.append(symbol) return clauses, symbols_set + def find_pure_symbols(clauses, symbols, model): """ - Return pure symbols and their assignments to satisfy the clause, if figurable. - Pure symbols are symbols in a formula that exist only in one form, either complemented or otherwise. + Return pure symbols and their values to satisfy clause. + Pure symbols are symbols in a formula that exist only + in one form, either complemented or otherwise. For example, - { { A4 , A3 , A5' , A1 , A3' } , { A4 } , { A3 } } has the pure symbols A4, A5' and A1. + { { A4 , A3 , A5' , A1 , A3' } , { A4 } , { A3 } } has + pure symbols A4, A5' and A1. This has the following steps: - 1. Ignore clauses that have already evaluated to be True. + 1. Ignore clauses that have already evaluated to be True. 2. Find symbols that occur only in one form in the rest of the clauses. - 3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively. - + 3. Assign value True or False depending on whether the symbols occurs + in normal or complemented form respectively. + >>> c1 = Clause(["A1", "A2'", "A3"]) >>> c2 = Clause(["A5'", "A2'", "A1"]) >>> f = Formula([c1, c2]) >>> c, s = generate_parameters(f) - + >>> model = {} >>> p, v = find_pure_symbols(c, s, model) >>> print(p, v) @@ -226,38 +240,42 @@ def find_pure_symbols(clauses, symbols, model): pure_symbols = [] assignment = dict() literals = [] - + for clause in clauses: - if clause.evaluate(model) == True: + if clause.evaluate(model) is True: continue - for l in clause.literals.keys(): - literals.append(l) + for literal in clause.literals.keys(): + literals.append(literal) for s in symbols: - sym = (s + "'") - if (s in literals and sym not in literals) or (s not in literals and sym in literals): + sym = s + "'" + if (s in literals and sym not in literals) or ( + s not in literals and sym in literals + ): pure_symbols.append(s) for p in pure_symbols: assignment[p] = None for s in pure_symbols: - sym = (s + "'") + sym = s + "'" if s in literals: assignment[s] = True elif sym in literals: assignment[s] = False return pure_symbols, assignment + def find_unit_clauses(clauses, model): """ - Returns the unit symbols and their assignments to satisfy the clause, if figurable. + Returns the unit symbols and their values to satisfy clause. Unit symbols are symbols in a formula that are: - - Either the only symbol in a clause - - Or all other literals in that clause have been assigned False + - Either the only symbol in a clause + - Or all other literals in that clause have been assigned False This has the following steps: 1. Find symbols that are the only occurences in a clause. - 2. Find symbols in a clause where all other literals are assigned to be False. - 3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively. - + 2. Find symbols in a clause where all other literals are assigned False. + 3. Assign True or False depending on whether the symbols occurs in + normal or complemented form respectively. + >>> c1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) >>> c2 = Clause(["A4"]) >>> c3 = Clause(["A3"]) @@ -277,11 +295,11 @@ def find_unit_clauses(clauses, model): unit_symbols.append(list(clause.literals.keys())[0]) else: Fcount, Ncount = 0, 0 - for l,v in clause.literals.items(): - if v == False: + for literal, value in clause.literals.items(): + if value is False: Fcount += 1 - elif v == None: - sym = l + elif value is None: + sym = literal Ncount += 1 if Fcount == clause.no_of_literals - 1 and Ncount == 1: unit_symbols.append(sym) @@ -296,6 +314,7 @@ def find_unit_clauses(clauses, model): return unit_symbols, assignment + def dpll_algorithm(clauses, symbols, model): """ Returns the model if the formula is satisfiable, else None @@ -321,20 +340,20 @@ def dpll_algorithm(clauses, symbols, model): check_clause_all_true = True for clause in clauses: clause_check = clause.evaluate(model) - if clause_check == False: + if clause_check is False: return False, None - elif clause_check == None: + elif clause_check is None: check_clause_all_true = False continue if check_clause_all_true: return True, model - + pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) P = None if len(pure_symbols) > 0: P, value = pure_symbols[0], assignment[pure_symbols[0]] - + if P: tmp_model = model tmp_model[P] = value @@ -342,14 +361,14 @@ def dpll_algorithm(clauses, symbols, model): if P in tmp_symbols: tmp_symbols.remove(P) return dpll_algorithm(clauses, tmp_symbols, tmp_model) - - unit_symbols, assignment = find_unit_clauses(clauses, model) + + unit_symbols, assignment = find_unit_clauses(clauses, model) P = None if len(unit_symbols) > 0: P, value = unit_symbols[0], assignment[unit_symbols[0]] if P: tmp_model = model - tmp_model[P]=value + tmp_model[P] = value tmp_symbols = [i for i in symbols] if P in tmp_symbols: tmp_symbols.remove(P) @@ -361,12 +380,14 @@ def dpll_algorithm(clauses, symbols, model): return dpll_algorithm(clauses, rest, tmp1) or dpll_algorithm(clauses, rest, tmp2) + if __name__ == "__main__": import doctest + doctest.testmod() formula = generate_formula() - print(f'The formula {formula} is', end = " ") + print(f"The formula {formula} is", end=" ") clauses, symbols = generate_parameters(formula) From e95dd936afe002f997f226d9e1cc6ddfc43f8e6b Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Sat, 7 Nov 2020 18:24:30 +0530 Subject: [PATCH 4/8] Codespell hook --- other/dpll.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/other/dpll.py b/other/dpll.py index b971531c2748..0264f73ec021 100644 --- a/other/dpll.py +++ b/other/dpll.py @@ -271,7 +271,7 @@ def find_unit_clauses(clauses, model): - Either the only symbol in a clause - Or all other literals in that clause have been assigned False This has the following steps: - 1. Find symbols that are the only occurences in a clause. + 1. Find symbols that are the only occurrences in a clause. 2. Find symbols in a clause where all other literals are assigned False. 3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively. From 33f370e97f38adc582cb47000662bb84f15ed7e9 Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Sun, 8 Nov 2020 14:00:26 +0530 Subject: [PATCH 5/8] Corrections part 2 --- other/dpll.py | 120 +++++++++++++++++++++++++------------------------- 1 file changed, 61 insertions(+), 59 deletions(-) diff --git a/other/dpll.py b/other/dpll.py index 0264f73ec021..2b7c0d3419bd 100644 --- a/other/dpll.py +++ b/other/dpll.py @@ -9,6 +9,7 @@ """ import random +from typing import List, Dict class Clause: @@ -31,7 +32,7 @@ class Clause: True """ - def __init__(self, literals): + def __init__(self, literals: List[int]) -> None: """ Represent the literals and an assignment in a clause." """ @@ -39,7 +40,7 @@ def __init__(self, literals): self.literals = {literal: None for literal in literals} self.no_of_literals = len(self.literals) - def __str__(self): + def __str__(self) -> str: """ To print a clause as in CNF. Variable clause holds the string representation. @@ -53,7 +54,7 @@ def __str__(self): return clause - def assign(self, model): + def assign(self, model: Dict[str, bool]) -> None: """ Assign values to literals of the clause as given by model. """ @@ -72,7 +73,7 @@ def assign(self, model): self.literals[list(self.literals.keys())[i]] = val i += 1 - def evaluate(self, model): + def evaluate(self, model: Dict[str, bool]) -> bool: """ Evaluates the clause with the assignments in model. This has the following steps: @@ -81,23 +82,21 @@ def evaluate(self, model): 3. Return None(unable to complete evaluation) if a literal has no assignment. 4. Compute disjunction of all values assigned in clause. """ - for literal in list(self.literals.keys()): + for literal in self.literals: if len(literal) == 2: symbol = literal + "'" - if symbol in list(self.literals.keys()): + if symbol in self.literals: return True else: symbol = literal[:2] - if symbol in list(self.literals.keys()): + if symbol in self.literals: return True self.assign(model) result = False for j in self.literals.values(): - if j is True: - return True - elif j is None: - return None + if j in (True, None): + return j for j in self.literals.values(): result = result or j return result @@ -111,37 +110,39 @@ class Formula: {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1)) Create two clauses and a formula with them - >>> c1 = Clause(["A1", "A2'", "A3"]) - >>> c2 = Clause(["A5'", "A2'", "A1"]) + >>> clause1 = Clause(["A1", "A2'", "A3"]) + >>> clause2 = Clause(["A5'", "A2'", "A1"]) - >>> f = Formula([c1, c2]) - >>> print(f) - { { A1 , A2' , A3 } , { A5' , A2' , A1 } } + >>> formula = Formula([clause1, clause2]) + >>> print(formula) + {{ A1 , A2' , A3 } , { A5' , A2' , A1 }} """ - def __init__(self, clauses): + def __init__(self, clauses: List[Clause]) -> None: """ Represent the number of clauses and the clauses themselves. """ self.clauses = [c for c in clauses] self.no_of_clauses = len(self.clauses) - def __str__(self): + def __str__(self) -> str: """ To print a formula as in CNF. Variable formula holds the string representation. """ - formula = "{ " - for i in range(0, self.no_of_clauses): - formula += str(self.clauses[i]) + " " - if i != self.no_of_clauses - 1: - formula += ", " + formula = "{" + clause_repr = " , " + clauses_as_strings = [str(clause) for clause in self.clauses] + + clause_repr = clause_repr.join(clauses_as_strings) + + formula += clause_repr formula += "}" return formula -def generate_clause(): +def generate_clause() -> Clause: """ Randomly generate a clause. All literals have the name Ax, where x is an integer from 1 to 5. @@ -161,11 +162,10 @@ def generate_clause(): else: literals.append(var_name) i += 1 - clause = Clause(literals) - return clause + return Clause(literals) -def generate_formula(): +def generate_formula() -> Formula: """ Randomly generate a formula. """ @@ -179,11 +179,10 @@ def generate_formula(): else: clauses.append(clause) i += 1 - formula = Formula(set(clauses)) - return formula + return Formula(set(clauses)) -def generate_parameters(formula): +def generate_parameters(formula: Formula) -> (List[Clause], List[str]): """ Return the clauses and symbols from a formula. A symbol is the uncomplemented form of a literal. @@ -191,28 +190,30 @@ def generate_parameters(formula): Symbol of A3 is A3. Symbol of A5' is A5. - >>> c1 = Clause(["A1", "A2'", "A3"]) - >>> c2 = Clause(["A5'", "A2'", "A1"]) + >>> clause1 = Clause(["A1", "A2'", "A3"]) + >>> clause2 = Clause(["A5'", "A2'", "A1"]) - >>> f = Formula([c1, c2]) - >>> c, s = generate_parameters(f) - >>> l = [str(i) for i in c] - >>> print(l) + >>> formula = Formula([clause1, clause2]) + >>> clauses, symbols = generate_parameters(formula) + >>> clauses_list = [str(i) for i in clauses] + >>> print(clauses_list) ["{ A1 , A2' , A3 }", "{ A5' , A2' , A1 }"] - >>> print(s) + >>> print(symbols) ['A1', 'A2', 'A3', 'A5'] """ clauses = formula.clauses symbols_set = [] for clause in formula.clauses: - for literal in clause.literals.keys(): + for literal in clause.literals: symbol = literal[:2] if symbol not in symbols_set: symbols_set.append(symbol) return clauses, symbols_set -def find_pure_symbols(clauses, symbols, model): +def find_pure_symbols( + clauses: List[Clause], symbols: List[str], model: Dict[str, bool] +) -> (List[str], Dict[str, bool]): """ Return pure symbols and their values to satisfy clause. Pure symbols are symbols in a formula that exist only @@ -226,15 +227,15 @@ def find_pure_symbols(clauses, symbols, model): 3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively. - >>> c1 = Clause(["A1", "A2'", "A3"]) - >>> c2 = Clause(["A5'", "A2'", "A1"]) + >>> clause1 = Clause(["A1", "A2'", "A3"]) + >>> clause2 = Clause(["A5'", "A2'", "A1"]) - >>> f = Formula([c1, c2]) - >>> c, s = generate_parameters(f) + >>> formula = Formula([clause1, clause2]) + >>> clauses, symbols = generate_parameters(formula) >>> model = {} - >>> p, v = find_pure_symbols(c, s, model) - >>> print(p, v) + >>> pure_symbols, values = find_pure_symbols(clauses, symbols, model) + >>> print(pure_symbols, values) ['A1', 'A2', 'A3', 'A5'] {'A1': True, 'A2': False, 'A3': True, 'A5': False} """ pure_symbols = [] @@ -244,7 +245,7 @@ def find_pure_symbols(clauses, symbols, model): for clause in clauses: if clause.evaluate(model) is True: continue - for literal in clause.literals.keys(): + for literal in clause.literals: literals.append(literal) for s in symbols: @@ -264,7 +265,9 @@ def find_pure_symbols(clauses, symbols, model): return pure_symbols, assignment -def find_unit_clauses(clauses, model): +def find_unit_clauses( + clauses: List[Clause], model: Dict[str, bool] +) -> (List[str], Dict[str, bool]): """ Returns the unit symbols and their values to satisfy clause. Unit symbols are symbols in a formula that are: @@ -276,17 +279,17 @@ def find_unit_clauses(clauses, model): 3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively. - >>> c1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) - >>> c2 = Clause(["A4"]) - >>> c3 = Clause(["A3"]) + >>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) + >>> clause2 = Clause(["A4"]) + >>> clause3 = Clause(["A3"]) - >>> f = Formula([c1, c2, c3]) - >>> c, s = generate_parameters(f) + >>> formula = Formula([clause1, clause2, clause3]) + >>> clauses, symbols = generate_parameters(formula) >>> model = {} - >>> u, v = find_unit_clauses(c, model) + >>> unit_clauses, values = find_unit_clauses(clauses, model) - >>> print(u, v) + >>> print(unit_clauses, values) ['A4', 'A3'] {'A4': True, 'A3': True} """ unit_symbols = [] @@ -306,16 +309,15 @@ def find_unit_clauses(clauses, model): assignment = dict() for i in unit_symbols: symbol = i[:2] - if len(i) == 2: - assignment[symbol] = True - else: - assignment[symbol] = False + assignment[symbol] = len(i) == 2 unit_symbols = [i[:2] for i in unit_symbols] return unit_symbols, assignment -def dpll_algorithm(clauses, symbols, model): +def dpll_algorithm( + clauses: List[Clause], symbols: List[str], model: Dict[str, bool] +) -> (bool, Dict[str, bool]): """ Returns the model if the formula is satisfiable, else None This has the following steps: From 3bae8f4d67b3e7beb48152cd85e56031c3a466c7 Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Sun, 8 Nov 2020 14:03:47 +0530 Subject: [PATCH 6/8] Corrections v2 --- other/dpll.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/other/dpll.py b/other/dpll.py index 2b7c0d3419bd..b6dba808d157 100644 --- a/other/dpll.py +++ b/other/dpll.py @@ -9,7 +9,7 @@ """ import random -from typing import List, Dict +from typing import Dict, List class Clause: @@ -54,7 +54,7 @@ def __str__(self) -> str: return clause - def assign(self, model: Dict[str, bool]) -> None: + def assign(self, model: Dict[str, bool]) -> None: """ Assign values to literals of the clause as given by model. """ From 3a0d65b8fcbf127b91c079db55e31a3bbb6aced4 Mon Sep 17 00:00:00 2001 From: Shivanirudh Date: Sun, 8 Nov 2020 18:26:22 +0530 Subject: [PATCH 7/8] Corrections v3 --- other/dpll.py | 102 +++++++++++++++++--------------------------------- 1 file changed, 34 insertions(+), 68 deletions(-) diff --git a/other/dpll.py b/other/dpll.py index b6dba808d157..ec3098546f08 100644 --- a/other/dpll.py +++ b/other/dpll.py @@ -2,7 +2,7 @@ Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, -i.e, for solving the CNF-SAT problem. +i.e, for solving the Conjunctive Normal Form SATisfiability(CNF-SAT) problem. For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm @@ -21,14 +21,12 @@ class Clause: {A5', A2', A1} is the clause (A5' v A2' v A1) Create a set of literals and a clause with them - >>> literals = ["A1", "A2'", "A3"] - >>> clause = Clause(literals) - >>> print(clause) - { A1 , A2' , A3 } + >>> str(Clause(["A1", "A2'", "A3"])) + "{A1 , A2' , A3}" Create model - >>> model = {"A1": True} - >>> clause.evaluate(model) + >>> clause = Clause(["A1", "A2'", "A3"]) + >>> clause.evaluate({"A1": True}) True """ @@ -43,16 +41,8 @@ def __init__(self, literals: List[int]) -> None: def __str__(self) -> str: """ To print a clause as in CNF. - Variable clause holds the string representation. """ - clause = "{ " - for i in range(0, self.no_of_literals): - clause += str(list(self.literals.keys())[i]) + " " - if i != self.no_of_literals - 1: - clause += ", " - clause += "}" - - return clause + return "{" + " , ".join(self.literals) + "}" def assign(self, model: Dict[str, bool]) -> None: """ @@ -110,12 +100,9 @@ class Formula: {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1)) Create two clauses and a formula with them - >>> clause1 = Clause(["A1", "A2'", "A3"]) - >>> clause2 = Clause(["A5'", "A2'", "A1"]) - - >>> formula = Formula([clause1, clause2]) - >>> print(formula) - {{ A1 , A2' , A3 } , { A5' , A2' , A1 }} + >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]) + >>> str(formula) + "{{A1 , A2' , A3} , {A5' , A2' , A1}}" """ def __init__(self, clauses: List[Clause]) -> None: @@ -128,18 +115,8 @@ def __init__(self, clauses: List[Clause]) -> None: def __str__(self) -> str: """ To print a formula as in CNF. - Variable formula holds the string representation. """ - formula = "{" - clause_repr = " , " - clauses_as_strings = [str(clause) for clause in self.clauses] - - clause_repr = clause_repr.join(clauses_as_strings) - - formula += clause_repr - formula += "}" - - return formula + return "{" + " , ".join(str(clause) for clause in self.clauses) + "}" def generate_clause() -> Clause: @@ -190,15 +167,12 @@ def generate_parameters(formula: Formula) -> (List[Clause], List[str]): Symbol of A3 is A3. Symbol of A5' is A5. - >>> clause1 = Clause(["A1", "A2'", "A3"]) - >>> clause2 = Clause(["A5'", "A2'", "A1"]) - - >>> formula = Formula([clause1, clause2]) + >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]) >>> clauses, symbols = generate_parameters(formula) >>> clauses_list = [str(i) for i in clauses] - >>> print(clauses_list) - ["{ A1 , A2' , A3 }", "{ A5' , A2' , A1 }"] - >>> print(symbols) + >>> clauses_list + ["{A1 , A2' , A3}", "{A5' , A2' , A1}"] + >>> symbols ['A1', 'A2', 'A3', 'A5'] """ clauses = formula.clauses @@ -227,16 +201,14 @@ def find_pure_symbols( 3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively. - >>> clause1 = Clause(["A1", "A2'", "A3"]) - >>> clause2 = Clause(["A5'", "A2'", "A1"]) - - >>> formula = Formula([clause1, clause2]) + >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]) >>> clauses, symbols = generate_parameters(formula) - >>> model = {} - >>> pure_symbols, values = find_pure_symbols(clauses, symbols, model) - >>> print(pure_symbols, values) - ['A1', 'A2', 'A3', 'A5'] {'A1': True, 'A2': False, 'A3': True, 'A5': False} + >>> pure_symbols, values = find_pure_symbols(clauses, symbols, {}) + >>> pure_symbols + ['A1', 'A2', 'A3', 'A5'] + >>> values + {'A1': True, 'A2': False, 'A3': True, 'A5': False} """ pure_symbols = [] assignment = dict() @@ -282,15 +254,13 @@ def find_unit_clauses( >>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) >>> clause2 = Clause(["A4"]) >>> clause3 = Clause(["A3"]) + >>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3])) - >>> formula = Formula([clause1, clause2, clause3]) - >>> clauses, symbols = generate_parameters(formula) - - >>> model = {} - >>> unit_clauses, values = find_unit_clauses(clauses, model) - - >>> print(unit_clauses, values) - ['A4', 'A3'] {'A4': True, 'A3': True} + >>> unit_clauses, values = find_unit_clauses(clauses, {}) + >>> unit_clauses + ['A4', 'A3'] + >>> values + {'A4': True, 'A3': True} """ unit_symbols = [] for clause in clauses: @@ -326,18 +296,14 @@ def dpll_algorithm( 3. Find pure symbols. 4. Find unit symbols. - >>> c1 = Clause(["A4", "A3", "A5'", "A1", "A3'"]) - >>> c2 = Clause(["A4"]) - >>> c3 = Clause(["A3"]) - - >>> f = Formula([c1, c2, c3]) - >>> c, s = generate_parameters(f) - - >>> model = {} - >>> soln, model = dpll_algorithm(c, s, model) + >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])]) + >>> clauses, symbols = generate_parameters(formula) - >>> print(soln, model) - True {'A4': True, 'A3': True} + >>> soln, model = dpll_algorithm(clauses, symbols, {}) + >>> soln + True + >>> model + {'A4': True} """ check_clause_all_true = True for clause in clauses: @@ -389,7 +355,7 @@ def dpll_algorithm( doctest.testmod() formula = generate_formula() - print(f"The formula {formula} is", end=" ") + print(f"The formula \n{formula}\n is", end=" ") clauses, symbols = generate_parameters(formula) From cc7441760ef12a6f09b95c75881ad81dcbe4961a Mon Sep 17 00:00:00 2001 From: Christian Clauss Date: Sun, 8 Nov 2020 17:32:42 +0100 Subject: [PATCH 8/8] =?UTF-8?q?Update=20and=20rename=20dpll.py=20to=20davi?= =?UTF-8?q?s=E2=80=93putnam=E2=80=93logemann=E2=80=93loveland.py?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...42\200\223logemann\342\200\223loveland.py" | 119 ++++++++---------- 1 file changed, 54 insertions(+), 65 deletions(-) rename other/dpll.py => "other/davis\342\200\223putnam\342\200\223logemann\342\200\223loveland.py" (79%) diff --git a/other/dpll.py "b/other/davis\342\200\223putnam\342\200\223logemann\342\200\223loveland.py" similarity index 79% rename from other/dpll.py rename to "other/davis\342\200\223putnam\342\200\223logemann\342\200\223loveland.py" index ec3098546f08..d16de6dd988b 100644 --- a/other/dpll.py +++ "b/other/davis\342\200\223putnam\342\200\223logemann\342\200\223loveland.py" @@ -1,11 +1,12 @@ +#!/usr/bin/env python3 + """ -Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, -backtracking-based search algorithm for deciding the satisfiability of -propositional logic formulae in conjunctive normal form, -i.e, for solving the Conjunctive Normal Form SATisfiability(CNF-SAT) problem. +Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based +search algorithm for deciding the satisfiability of propositional logic formulae in +conjunctive normal form, i.e, for solving the Conjunctive Normal Form SATisfiability +(CNF-SAT) problem. -For more information about the algorithm: -https://en.wikipedia.org/wiki/DPLL_algorithm +For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm """ import random @@ -14,16 +15,12 @@ class Clause: """ - A clause represented in CNF. + A clause represented in Conjunctive Normal Form. A clause is a set of literals, either complemented or otherwise. For example: {A1, A2, A3'} is the clause (A1 v A2 v A3') {A5', A2', A1} is the clause (A5' v A2' v A1) - Create a set of literals and a clause with them - >>> str(Clause(["A1", "A2'", "A3"])) - "{A1 , A2' , A3}" - Create model >>> clause = Clause(["A1", "A2'", "A3"]) >>> clause.evaluate({"A1": True}) @@ -36,32 +33,40 @@ def __init__(self, literals: List[int]) -> None: """ # Assign all literals to None initially self.literals = {literal: None for literal in literals} - self.no_of_literals = len(self.literals) def __str__(self) -> str: """ - To print a clause as in CNF. + To print a clause as in Conjunctive Normal Form. + >>> str(Clause(["A1", "A2'", "A3"])) + "{A1 , A2' , A3}" """ return "{" + " , ".join(self.literals) + "}" + def __len__(self) -> int: + """ + To print a clause as in Conjunctive Normal Form. + >>> len(Clause([])) + 0 + >>> len(Clause(["A1", "A2'", "A3"])) + 3 + """ + return len(self.literals) + def assign(self, model: Dict[str, bool]) -> None: """ Assign values to literals of the clause as given by model. """ - i = 0 - while i < self.no_of_literals: - symbol = list(self.literals.keys())[i][:2] - if symbol in model.keys(): - val = model[symbol] + for literal in self.literals: + symbol = literal[:2] + if symbol in model: + value = model[symbol] else: - i += 1 continue - if val is not None: + if value is not None: # Complement assignment if literal is in complemented form - if list(self.literals.keys())[i][-1] == "'": - val = not val - self.literals[list(self.literals.keys())[i]] = val - i += 1 + if literal.endswith("'"): + value = not value + self.literals[literal] = value def evaluate(self, model: Dict[str, bool]) -> bool: """ @@ -73,48 +78,36 @@ def evaluate(self, model: Dict[str, bool]) -> bool: 4. Compute disjunction of all values assigned in clause. """ for literal in self.literals: - if len(literal) == 2: - symbol = literal + "'" - if symbol in self.literals: - return True - else: - symbol = literal[:2] - if symbol in self.literals: - return True + symbol = literal.rstrip("'") if literal.endswith("'") else literal + "'" + if symbol in self.literals: + return True self.assign(model) - result = False - for j in self.literals.values(): - if j in (True, None): - return j - for j in self.literals.values(): - result = result or j - return result + for value in self.literals.values(): + if value in (True, None): + return value + return any(self.literals.values()) class Formula: """ - A formula represented in CNF. + A formula represented in Conjunctive Normal Form. A formula is a set of clauses. For example, {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1)) - - Create two clauses and a formula with them - >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]) - >>> str(formula) - "{{A1 , A2' , A3} , {A5' , A2' , A1}}" """ def __init__(self, clauses: List[Clause]) -> None: """ Represent the number of clauses and the clauses themselves. """ - self.clauses = [c for c in clauses] - self.no_of_clauses = len(self.clauses) + self.clauses = list(clauses) def __str__(self) -> str: """ - To print a formula as in CNF. + To print a formula as in Conjunctive Normal Form. + str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])) + "{{A1 , A2' , A3} , {A5' , A2' , A1}}" """ return "{" + " , ".join(str(clause) for clause in self.clauses) + "}" @@ -146,16 +139,10 @@ def generate_formula() -> Formula: """ Randomly generate a formula. """ - clauses = [] + clauses = set() no_of_clauses = random.randint(1, 10) - i = 0 - while i < no_of_clauses: - clause = generate_clause() - if clause in clauses: - i -= 1 - else: - clauses.append(clause) - i += 1 + while len(clauses) < no_of_clauses: + clauses.add(generate_clause()) return Formula(set(clauses)) @@ -264,7 +251,7 @@ def find_unit_clauses( """ unit_symbols = [] for clause in clauses: - if clause.no_of_literals == 1: + if len(clause) == 1: unit_symbols.append(list(clause.literals.keys())[0]) else: Fcount, Ncount = 0, 0 @@ -274,7 +261,7 @@ def find_unit_clauses( elif value is None: sym = literal Ncount += 1 - if Fcount == clause.no_of_literals - 1 and Ncount == 1: + if Fcount == len(clause) - 1 and Ncount == 1: unit_symbols.append(sym) assignment = dict() for i in unit_symbols: @@ -317,7 +304,11 @@ def dpll_algorithm( if check_clause_all_true: return True, model - pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) + try: + pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) + except RecursionError: + print("raises a RecursionError and is") + return None, {} P = None if len(pure_symbols) > 0: P, value = pure_symbols[0], assignment[pure_symbols[0]] @@ -355,14 +346,12 @@ def dpll_algorithm( doctest.testmod() formula = generate_formula() - print(f"The formula \n{formula}\n is", end=" ") + print(f"The formula {formula} is", end=" ") clauses, symbols = generate_parameters(formula) - solution, model = dpll_algorithm(clauses, symbols, {}) if solution: - print(" satisfiable with the assignment: ") - print(model) + print(f"satisfiable with the assignment {model}.") else: - print(" not satisfiable") + print("not satisfiable.")