python 实现 leetcode 各种问题 课程设计 代码

#!/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. For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm """ from __future__ import annotations import random from collections.abc import Iterable class Clause: """ 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 model >>> clause = Clause(["A1", "A2'", "A3"]) >>> clause.evaluate({"A1": True}) True """ def __init__(self, literals: list[str]) -> None: """ Represent the literals and an assignment in a clause." """ # Assign all literals to None initially self.literals: dict[str, bool | None] = {literal: None for literal in literals} def __str__(self) -> str: """ 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]) -> None: """ Assign values to literals of the clause as given by model. """ for literal in self.literals: symbol = literal[:2] if symbol in model: value = model[symbol] else: continue if value is not None: # Complement assignment if literal is in complemented form if literal.endswith("'"): value = not value self.literals[literal] = value def evaluate(self, model: dict[str, bool | None]) -> bool | None: """ 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 literal in self.literals: symbol = literal.rstrip("'") if literal.endswith("'") else literal + "'" if symbol in self.literals: return True self.assign(model) for value in self.literals.values(): if value in (True, None): return value return any(self.literals.values()) class Formula: """ 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)) """ def __init__(self, clauses: Iterable[Clause]) -> None: """ Represent the number of clauses and the clauses themselves. """ self.clauses = list(clauses) def __str__(self) -> str: """ 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) + "}" def generate_clause() -> 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 return Clause(literals) def generate_formula() -> Formula: """ Randomly generate a formula. """ clauses: set[Clause] = set() no_of_clauses = random.randint(1, 10) while len(clauses) < no_of_clauses: clauses.add(generate_clause()) return Formula(clauses) def generate_parameters(formula: Formula) -> tuple[list[Clause], list[str]]: """ 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. >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]) >>> clauses, symbols = generate_parameters(formula) >>> clauses_list = [str(i) for i in clauses] >>> clauses_list ["{A1 , A2' , A3}", "{A5' , A2' , A1}"] >>> symbols ['A1', 'A2', 'A3', '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: list[Clause], symbols: list[str], model: dict[str, bool | None] ) -> tuple[list[str], dict[str, bool | None]]: """ 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 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. >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]) >>> clauses, symbols = generate_parameters(formula) >>> 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[str, bool | None] = {} literals = [] for clause in clauses: if clause.evaluate(model): continue for literal in clause.literals: 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 ): 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: list[Clause], model: dict[str, bool | None] ) -> tuple[list[str], dict[str, bool | None]]: """ 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 This has the following steps: 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. >>> clause1 = Clause(["A4", "A3", "A5'",