Untitled
unknown
plain_text
a year ago
3.6 kB
4
Indexable
///a. PL-Resolution def pl_resolution(kb, alpha): clauses = kb + [negate(alpha)] new = set() while True: n = len(clauses) for i in range(n): for j in range(i + 1, n): resolvents = resolve(clauses[i], clauses[j]) if [] in resolvents: return True new.update(resolvents) if new.issubset(set(clauses)): return False clauses.extend(new) def resolve(ci, cj): resolvents = [] for di in ci: for dj in cj: if di == negate(dj): resolvent = set(ci).union(set(cj)) resolvent.remove(di) resolvent.remove(dj) resolvents.append(list(resolvent)) return resolvents def negate(literal): if literal.startswith('~'): return literal[1:] else: return '~' + literal ///DPLL def dpll(clauses, assignment={}): clauses, unit_clauses = unit_propagate(clauses) if [] in clauses: return False, {} if not clauses: return True, assignment literal = select_literal(clauses) new_clauses = [c for c in clauses if literal not in c] new_clauses = [list(set(c) - {negate(literal)}) for c in new_clauses] sat, final_assignment = dpll(new_clauses, {**assignment, literal: True}) if sat: return True, final_assignment new_clauses = [c for c in clauses if negate(literal) not in c] new_clauses = [list(set(c) - {literal}) for c in new_clauses] return dpll(new_clauses, {**assignment, negate(literal): True}) def unit_propagate(clauses): assignment = {} unit_clauses = [c for c in clauses if len(c) == 1] while unit_clauses: unit = unit_clauses.pop() literal = unit[0] assignment[literal] = True clauses = [c for c in clauses if literal not in c] for clause in clauses: if negate(literal) in clause: clause.remove(negate(literal)) unit_clauses = [c for c in clauses if len(c) == 1] return clauses, assignment def select_literal(clauses): for clause in clauses: for literal in clause: return literal ////WalkSAT import random def walksat(clauses, max_flips, p=0.5): model = {literal: random.choice([True, False]) for clause in clauses for literal in clause} for _ in range(max_flips): satisfied_clauses = [clause for clause in clauses if any(model[literal] for literal in clause)] if len(satisfied_clauses) == len(clauses): return True, model clause = random.choice([clause for clause in clauses if clause not in satisfied_clauses]) if random.random() < p: literal = random.choice(clause) else: literal = min(clause, key=lambda l: len([c for c in clauses if l in c])) model[literal] = not model[literal] return False, model ///So sánh thời gian thực thi của các thuật toán import time def compare_algorithms(kb, alpha): algorithms = { "PL-Resolution": pl_resolution, "DPLL": dpll, "WalkSAT": walksat } results = {} for name, algorithm in algorithms.items(): start_time = time.time() if name == "WalkSAT": result = algorithm(kb, 1000) else: result = algorithm(kb, alpha) end_time = time.time() results[name] = end_time - start_time, result return results # Example usage: kb = [['p', '~q'], ['q', 'r'], ['~r', 's'], ['~p', '~s']] alpha = 'r' print(compare_algorithms(kb, alpha))
Editor is loading...
Leave a Comment