File code

def negate(literal):
    if literal.startswith('~'):
        return literal[1:]
    else:
        return '~' + literal

def resolve(ci, cj):
    resolvents = []
    for di in ci:
        for dj in cj:
            if di == negate(dj):
                resolvent = list(set(ci + cj) - {di, dj})
                resolvents.append(resolvent)
    return resolvents

def pl_resolution(kb, alpha):
    clauses = kb + [[negate(alpha)]]
    new = set()
    while True:
        n = len(clauses)
        pairs = [(clauses[i], clauses[j]) for i in range(n) for j in range(i + 1, n)]
        for (ci, cj) in pairs:
            resolvents = resolve(ci, cj)
            if [] in resolvents:
                return True
            new.update(map(tuple, resolvents))
        if new.issubset(set(map(tuple, clauses))):
            return False
        clauses.extend(map(list, new))

def unit_propagate(clauses, assignment):
    unit_clauses = [c for c in clauses if len(c) == 1]
    while unit_clauses:
        unit = unit_clauses[0]
        literal = unit[0]
        assignment[literal] = True
        clauses = substitute(clauses, literal)
        if [] in clauses:
            return clauses, assignment
        unit_clauses = [c for c in clauses if len(c) == 1]
    return clauses, assignment

def substitute(clauses, literal):
    new_clauses = []
    for clause in clauses:
        if literal in clause:
            continue
        new_clause = [l for l in clause if l != negate(literal)]
        new_clauses.append(new_clause)
    return new_clauses

def select_literal(clauses):
    for clause in clauses:
        for literal in clause:
            return literal

def dpll(clauses, assignment={}):
    clauses, assignment = unit_propagate(clauses, assignment)
    if any([len(c) == 0 for c in clauses]):
        return False
    if len(clauses) == 0:
        return True, assignment
    literal = select_literal(clauses)
    new_assignment = assignment.copy()
    new_assignment[literal] = True
    sat, final_assignment = dpll(substitute(clauses, literal), new_assignment)
    if sat:
        return True, final_assignment
    new_assignment[literal] = False
    return dpll(substitute(clauses, negate(literal)), new_assignment)

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.get(literal, False) 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

import time

def compare_algorithms(test_cases):
    results = []

    for kb, alpha in test_cases:
        test_result = {"KB": kb, "alpha": alpha}

        # PL-Resolution
        start_time = time.time()
        pl_result = pl_resolution(kb, alpha)
        end_time = time.time()
        test_result["PL-Resolution"] = {"result": pl_result, "time": end_time - start_time}

        # DPLL
        start_time = time.time()
        dpll_result, _ = dpll(kb)
        end_time = time.time()
        test_result["DPLL"] = {"result": dpll_result, "time": end_time - start_time}

        # WalkSAT
        start_time = time.time()
        walksat_result, _ = walksat(kb, 1000)  # Sử dụng 1000 flips cho WalkSAT
        end_time = time.time()
        test_result["WalkSAT"] = {"result": walksat_result, "time": end_time - start_time}

        results.append(test_result)

    return results

# Ví dụ sử dụng với các testcase mẫu
test_cases = [
    ([
        ['p', '~q'],
        ['q', 'r'],
        ['~r', 's'],
        ['~p', '~s']
    ], 'r'),
    ([
        ['a', '~b', 'c'],
        ['~a', 'b'],
        ['~b', '~c'],
        ['b', 'c']
    ], 'a'),
    ([
        ['x', '~y'],
        ['~x', 'z'],
        ['y', 'w'],
        ['~z', '~w']
    ], 'x'),
    ([
        ['m', 'n'],
        ['~m', 'o'],
        ['~n', 'p'],
        ['~o', '~p']
    ], 'm')
]

results = compare_algorithms(test_cases)

for result in results:
    print(f"Test case: KB={result['KB']}, alpha={result['alpha']}")
    for algo in ['PL-Resolution', 'DPLL', 'WalkSAT']:
        res = result[algo]['result']
        time_taken = result[algo]['time']
        print(f"{algo}: {'Yes' if res else 'No'}, Time taken: {time_taken:.6f} seconds")
    print()