কুক-লেভিন থিওরেম — SAT NP-কমপ্লিট

# Cook-Levin-স্টাইল এনকোডিং-এর একটি ছোট্ট, হাতে-তৈরি দৃষ্টান্ত -- সম্পূর্ণ সাধারণ নির্মাণ নয়
# L44-এর verify_sat পুনর্ব্যবহার করে (একই eval_formula লজিক, eval()/exec()/re ছাড়াই)

import itertools

def eval_formula(node, assignment):
    if isinstance(node, str):
        return assignment[node]
    op = node[0]
    if op == 'not':
        return not eval_formula(node[1], assignment)
    if op == 'and':
        return eval_formula(node[1], assignment) and eval_formula(node[2], assignment)
    if op == 'or':
        return eval_formula(node[1], assignment) or eval_formula(node[2], assignment)
    raise ValueError(f"অজানা অপারেটর: {op}")

def verify_sat(formula, assignment):
    return eval_formula(formula, assignment)

def var(t, p, s):
    return f"t{t}_p{p}_s{s}"

def conjunction(subformulas):
    result = subformulas[0]
    for f in subformulas[1:]:
        result = ('and', result, f)
    return result

def disjunction(subformulas):
    result = subformulas[0]
    for f in subformulas[1:]:
        result = ('or', result, f)
    return result

cells = [0, 1, 2]
symbols = ['0', '1', '_']
time_steps = [0, 1]   # t=0 (শুরু) -> t=1 (এক ধাপ পরে)

# একটি নির্দিষ্ট, দেওয়া ট্রানজিশন রুল -- পজিশন 0: '0' -> '1' (flip), বাকি সব identity;
# পজিশন 1, 2: সবসময় identity (অপরিবর্তিত থাকে)
rule = {
    0: {'0': '1', '1': '1', '_': '_'},
    1: {'0': '0', '1': '1', '_': '_'},
    2: {'0': '0', '1': '1', '_': '_'},
}

clauses = []

# (a) প্রতিটি সেল-সময়ে ঠিক একটি সিম্বল
for t in time_steps:
    for p in cells:
        vars_tp = [var(t, p, s) for s in symbols]
        clauses.append(disjunction(vars_tp))                    # at least one
        for s1, s2 in itertools.combinations(symbols, 2):
            clauses.append(('or', ('not', var(t, p, s1)), ('not', var(t, p, s2))))  # at most one

# (b) t -> t+1 ট্রানজিশন rule-এর সাথে সামঞ্জস্যপূর্ণ
for p in cells:
    for s in symbols:
        clauses.append(('or', ('not', var(0, p, s)), var(1, p, rule[p][s])))

phi = conjunction(clauses)
print(f"মোট ক্লজ সংখ্যা: {len(clauses)}")

def build_assignment(trace):
    assignment = {}
    for t in time_steps:
        for p in cells:
            for s in symbols:
                assignment[var(t, p, s)] = (trace[t][p] == s)
    return assignment

# আসল, সঠিক কম্পিউটেশন ট্রেস: t=0 টেপ = 0,1,_  ->  t=1 টেপ = 1,1,_  (rule অনুযায়ী পজিশন 0 ফ্লিপ হয়েছে)
correct_trace = {0: ['0', '1', '_'], 1: ['1', '1', '_']}
correct_assignment = build_assignment(correct_trace)
print("সঠিক কম্পিউটেশন ট্রেস phi সন্তুষ্ট করে?", verify_sat(phi, correct_assignment), "(প্রত্যাশিত: True)")

# ভুল ট্রেস: পজিশন 0 flip না হয়ে '0'-ই থেকে গেছে -- rule (b) লঙ্ঘন করে
wrong_trace = {0: ['0', '1', '_'], 1: ['0', '1', '_']}
wrong_assignment = build_assignment(wrong_trace)
print("ভুল কম্পিউটেশন ট্রেস phi সন্তুষ্ট করে?", verify_sat(phi, wrong_assignment), "(প্রত্যাশিত: False)")