Untitled

import random

def walksat(clauses, max_flips, prob):
    """
    WalkSAT algorithm to determine satisfiability of clauses within a limited number of flips.
    """
    n_vars = get_variable_count(clauses)
    assignment = random_assignment(n_vars)
    
    for _ in range(max_flips):
        if all(clause_satisfied(clause, assignment) for clause in clauses):
            return True, assignment  # All clauses satisfied
        
        unsatisfied_clauses = [clause for clause in clauses if not clause_satisfied(clause, assignment)]
        clause = random.choice(unsatisfied_clauses)
        
        if random.random() < prob:
            variable = random.choice(clause)
        else:
            variable = max(clause, key=lambda var: count_satisfied(clauses, assignment, var))
        
        assignment[abs(variable)] = not assignment.get(abs(variable))
    
    return False, assignment

def clause_satisfied(clause, assignment):
    """
    Check if a clause is satisfied with the current assignment.
    """
    for literal in clause:
        if literal > 0:
            if assignment.get(literal):
                return True
        else:
            if not assignment.get(-literal):
                return True
    return False

def count_satisfied(clauses, assignment, var):
    """
    Count the number of clauses satisfied if the given variable is flipped.
    """
    count = 0
    for clause in clauses:
        if var in clause:
            if clause_satisfied(clause, {**assignment, var: not assignment.get(var)}):
                count += 1
    return count

def random_assignment(n_vars):
    """
    Generate a random initial assignment for the variables.
    """
    return {var: random.choice([True, False]) for var in range(1, n_vars + 1)}

def get_variable_count(clauses):
    """
    Get the maximum variable index from the list of clauses.
    """
    return max(abs(literal) for clause in clauses for literal in clause)

# Testcases
testcases = [
    {
        "KB": [[1, 2], [-1, 3], [-2, -3]],
        "Alpha": 1,
        "Expected_Result": True,
        "Expected_Assignment": {1: True, 2: False, 3: True}
    },
    {
        "KB": [[1, -2], [-1, 3], [2, 3]],
        "Alpha": 1,
        "Expected_Result": False,
        "Expected_Assignment": None
    },
    {
        "KB": [[1, 2], [2, 3], [3, 1]],
        "Alpha": 1,
        "Expected_Result": True,
        "Expected_Assignment": {1: True, 2: False, 3: False}
    },
    {
        "KB": [[1, 2], [-2, 3], [3, -4], [-1, 4]],
        "Alpha": 3,
        "Expected_Result": True,
        "Expected_Assignment": {1: True, 2: False, 3: True, 4: False}
    },
    {
        "KB": [[1, 2], [-2, 3], [3, -4], [-1, 4]],
        "Alpha": 4,
        "Expected_Result": True,
        "Expected_Assignment": {1: True, 2: False, 3: True, 4: True}
    }
]

# Run testcases
for i, testcase in enumerate(testcases, start=1):
    print(f"Testcase {i}:")
    kb = testcase["KB"]
    alpha = testcase["Alpha"]
    expected_result = testcase["Expected_Result"]
    expected_assignment = testcase["Expected_Assignment"]
    
    result, assignment = walksat(kb, 1000, 0.5)
    
    print("Expected Result:", "YES" if expected_result else "NO")
    print("Expected Assignment:", expected_assignment)
    print("Actual Result:", "YES" if result else "NO")
    print("Actual Assignment:", assignment)
    print("-" * 50)