Untitled

///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))