আরও NP-কমপ্লিট প্রবলেম

# SAT (যেকোনো ক্লজ-দৈর্ঘ্য) থেকে 3-SAT-এ ক্লজ-স্প্লিটিং রিডাকশন -- বাস্তব, কার্যকর কোড
# লিটারেল প্রতিনিধিত্ব: স্ট্রিং, নেগেশনের জন্য সামনে '-' -- যেমন "x1" বা "-x1"

import itertools

def neg(lit):
    return lit[1:] if lit.startswith('-') else '-' + lit

def var_of(lit):
    return lit[1:] if lit.startswith('-') else lit

def all_vars(formula):
    vs = set()
    for clause in formula:
        for lit in clause:
            vs.add(var_of(lit))
    return sorted(vs)

def eval_formula(formula, assignment):
    # ফর্মুলা সত্য হয় শুধু তখনই যখন প্রতিটি ক্লজ সত্য (AND অফ ক্লজ)
    for clause in formula:
        clause_true = False
        for lit in clause:
            val = assignment[var_of(lit)]
            if lit.startswith('-'):
                val = not val
            if val:
                clause_true = True
                break
        if not clause_true:
            return False
    return True

def brute_force_sat(formula):
    # সব ভ্যারিয়েবলের সব সম্ভাব্য True/False কম্বিনেশন চেষ্টা করে সিদ্ধযোগ্যতা যাচাই
    vs = all_vars(formula)
    for bits in itertools.product([False, True], repeat=len(vs)):
        assignment = dict(zip(vs, bits))
        if eval_formula(formula, assignment):
            return True, assignment
    return False, None

def reduce_sat_to_3sat(formula):
    # প্রতিটি লম্বা ক্লজকে নতুন সহায়ক ভ্যারিয়েবল দিয়ে ৩-লিটারেল ক্লজের চেইনে ভাঙা হয়
    new_formula = []
    counter = [0]
    def fresh():
        counter[0] += 1
        return f"y{counter[0]}"
    for clause in formula:
        k = len(clause)
        if k <= 3:
            new_formula.append(list(clause))
            continue
        prev_aux = fresh()
        new_formula.append([clause[0], clause[1], prev_aux])
        for i in range(2, k - 2):
            new_aux = fresh()
            new_formula.append([neg(prev_aux), clause[i], new_aux])
            prev_aux = new_aux
        new_formula.append([neg(prev_aux), clause[k - 2], clause[k - 1]])
    return new_formula

def is_3cnf(formula):
    return all(len(clause) <= 3 for clause in formula)

# একটি ৫-লিটারেল ক্লজসহ একটি ফর্মুলা
formula = [
    ["x1", "x2", "x3", "x4", "x5"],   # দৈর্ঘ্য ৫ -- সাধারণ CNF-এ বৈধ, 3-SAT-এ নয়
    ["-x1"], ["-x2"], ["-x3"], ["-x4"],
]

sat_before, assign_before = brute_force_sat(formula)
print("মূল ফর্মুলা (সাধারণ CNF) সিদ্ধযোগ্য:", sat_before, "|", assign_before)

reduced = reduce_sat_to_3sat(formula)
print("\nরূপান্তরিত 3-SAT ক্লজসমূহ:")
for c in reduced:
    print(" ", c)
print("প্রতিটি ক্লজ <=3 লিটারেল:", is_3cnf(reduced))

sat_after, assign_after = brute_force_sat(reduced)
print("\nরূপান্তরিত ফর্মুলা সিদ্ধযোগ্য:", sat_after, "|", assign_after)

print("\n>> মূল ও রূপান্তরিত ফর্মুলার সিদ্ধযোগ্যতা মিলছে:", sat_before == sat_after)

# একটি UNSATISFIABLE কেসও যাচাই -- '-x5' যোগ করলে x5=True বাধ্যতাও ভেঙে যায়
unsat_formula = formula + [["-x5"]]
sat_u_before, _ = brute_force_sat(unsat_formula)
sat_u_after, _ = brute_force_sat(reduce_sat_to_3sat(unsat_formula))
print("UNSAT কেস -- মূল:", sat_u_before, "| রূপান্তরিত:", sat_u_after, "| মিলছে:", sat_u_before == sat_u_after)