কাজে যুক্তি — specification, ধাঁধা আর SAT solver

১ · কোডের শর্তে যুক্তি — সরল করা, short-circuit আর guard clause

এই মডিউলের আগের ছয়টি পর্বে আমরা যুক্তির ভাষা শিখেছি: proposition আর truth table (পর্ব ০২), logical equivalence-এর নিয়ম (পর্ব ০৩), quantifier (পর্ব ০৪ আর পর্ব ০৫), অনুমানের নিয়ম (পর্ব ০৬)। এই শেষ পর্বে দেখব, সেই ভাষা প্রতিদিনের কাজে কোথায় লাগে: প্রোগ্রামের শর্তে, নিয়মের তালিকায়, ধাঁধায়, আর এমন যন্ত্রে যা লাখো variable-এর সূত্র সমাধান করে।

শুরু করি বাজারঘরের চেকআউট কোড থেকে। একজন প্রোগ্রামার ফ্রি ডেলিভারির শর্ত লিখেছেন, কয়েকবার জোড়াতালি দেওয়ার পর যা দাঁড়িয়েছে এরকম:

if not (not is_member and total < 1000) and not (is_remote and not is_member):
    fee = 0

লাইনটি পড়ে কেউ এক নজরে বলতে পারবেন না, কে ফ্রি ডেলিভারি পান। যুক্তির ভাষায় আনি: m = “ক্রেতা সদস্য”, b = “অর্ডার ১০০০ টাকা বা বেশি” (তাই total < 1000 মানে ¬b), r = “ঠিকানা দূরের জেলায়”। শর্তটি তখন

¬(¬m ∧ ¬b) ∧ ¬(r ∧ ¬m)

পর্ব ০৩-এর নিয়মগুলো দিয়ে এটিকে ধাপে ধাপে সরল করি। প্রতিটি ধাপে ঠিক একটি নিয়ম খাটবে, আর পাশে লেখা থাকবে কোন নিয়ম। “পরে” চাপুন:

1কোড → সূত্র2De Morgan3Double negation4Commutative5Distributive6সূত্র → কোড

প্রতিটি ধাপ একটি প্রমাণিত সমতা, তাই শেষ রূপটি প্রথমটির সমান: এটিই প্রমাণ। তবু পরীক্ষা করে নেওয়া সস্তা। নিচের ব্লক ৮টি সারিতে দুটি রূপ মেলায়, একটি সাধারণ ভুল “সরলীকরণ” ধরে, আর short-circuit কীভাবে কাজ করে তা দেখায়। প্রথমবার চালালে ব্রাউজারে Python (Pyodide) নামতে কয়েক সেকেন্ড লাগে, পরে দ্রুত চলে।

from itertools import product

imp = lambda a, b: (not a) or b
# m = সদস্য, b = অর্ডার ১০০০ টাকা বা বেশি, r = দূরের জেলা
messy = lambda m, b, r: not (not m and not b) and not (r and not m)
clean = lambda m, b, r: m or (b and not r)
wrong = lambda m, b, r: (m and b) and not (r and not m)   # De Morgan ভুল

for name, f in [("clean", clean), ("wrong", wrong)]:
    bad = [row for row in product([True, False], repeat=3)
           if messy(*row) != f(*row)]
    print(f"messy vs {name}: {8 - len(bad)} of 8 rows agree", bad)

# nested if  ≡  একসঙ্গে শর্ত:  p → (q → r)  ≡  (p ∧ q) → r
print("exportation:", all(imp(p, imp(q, r)) == imp(p and q, r)
                          for p, q, r in product([True, False], repeat=3)))

def is_member(cid):                 # ধীর কাজের ভান: ডাটাবেস খোঁজা
    print("   looked up member", cid)
    return cid == 7

for total in (1200, 300):
    print("total", total)
    print("   free:", total >= 1000 or is_member(7))

order = None                        # None হলে .get() চালানোই হয় না
print("guarded:", order is not None and order.get("total", 0) > 500)

messy vs clean: 8 of 8 rows agree []
messy vs wrong: 5 of 8 rows agree [(True, False, True), (True, False, False), (False, True, False)]
exportation: True
total 1200
   free: True
total 300
   looked up member 7
   free: True
guarded: False

Short-circuit: কোডের ∧ গণিতের ∧-এর চেয়ে একটু বেশি

Python, C, Java, JavaScript-এর মতো বেশিরভাগ ভাষায় and/&& আর or/|| short-circuit করে: বাঁ দিক দেখেই উত্তর জানা গেলে ডান দিক হিসাবই হয় না। Truth table-এর ভাষায় এটি নিরাপদ, কারণ x = F হলে x ∧ y = F, y যা-ই হোক। কিন্তু একটি সূক্ষ্ম পার্থক্য আছে। গণিতে x ∧ y ≡ y ∧ x (commutative). কোডে order is not None and order.total > 500 নিরাপদ, অথচ ক্রম উল্টালে order.total > 500 and order is not None None-এর ক্ষেত্রে error দেয়। কারণ কোডের একটি অংশ “অসংজ্ঞায়িত” হতে পারে (error, অসীম লুপ, ধীর ডাটাবেস কল), যা দুই-মানের truth table-এ নেই। নিয়ম: যে শর্ত পরের অংশকে নিরাপদ করে, সেটি বাঁয়ে লিখুন। Python-এর শর্ত লেখার বিস্তারিত Python প্রোগ্রামিং কোর্সের পর্ব ১১-এ।

Guard clause আর exportation নিয়ম

অনেক স্তরের nested if পড়া কঠিন। Guard clause মানে ফাংশনের শুরুতেই বাদ পড়ার ক্ষেত্রগুলো সরিয়ে দেওয়া:

# আগে: তিন স্তরের nesting
if order is not None:
    if order.paid:
        if not order.cancelled:
            ship(order)

# পরে: guard clause
if order is None or not order.paid or order.cancelled:
    return
ship(order)

দুটি রূপ যে একই কাজ করে, সেটি যুক্তির দুটি নিয়মের ফল। প্রথমত, nested if মানে p → (q → (s → ship)), আর exportation নিয়মে p → (q → r) ≡ (p ∧ q) → r, তাই পুরোটা (p ∧ q ∧ s) → ship. দ্বিতীয়ত, guard-এর শর্ত ¬p ∨ ¬q ∨ ¬s, De Morgan-এ যা ¬(p ∧ q ∧ s): ঠিক যে ক্ষেত্রে ship হবে না। কোড পরিষ্কার রাখার আরও কৌশল সফটওয়্যার ইঞ্জিনিয়ারিং ও Git কোর্সের পর্ব ৪২-এ।

২ · Specification — পরস্পরবিরোধী নিয়ম আর তার ক্ষুদ্রতম কারণ

পর্ব ০২-এ দেখেছেন, একগুচ্ছ নিয়ম consistent যদি অন্তত একটি মান-বসানো সবকটিকে একসঙ্গে সত্য করে। অর্থাৎ specification-এর consistency প্রশ্নটি আসলে নিয়মগুলোর ∧ satisfiable কি না, সেই প্রশ্ন। এবার দুটি নতুন প্রশ্ন তুলি: কখন বিরোধ হতেই পারে না, আর বিরোধ হলে দোষী কোন নিয়মগুলো।

প্রমাণ:

1. সব variable = F ধরি। তাহলে প্রতিটি negative literal ¬x-এর মান ¬F = T.
2. একটি clause হলো literal-গুলোর ∨; তার অন্তত একটি literal T হলেই clause T.
3. ধরে নেওয়া হয়েছে প্রতিটি clause-এ অন্তত একটি negative literal আছে, যা ধাপ ১ অনুযায়ী T. তাই প্রতিটি clause T, আর তাদের ∧-ও T. ∎

এর অর্থ কাজের: “h হলে ¬u” (¬h ∨ ¬u) বা “p হলে u” (¬p ∨ u) ধরনের নিষেধ আর শর্তসাপেক্ষ নিয়ম যত খুশি থাকুক, “কিছুই না করা” সবসময় একটি সমাধান। বিরোধ জন্মাতে হলে অন্তত একটি বাধ্যতামূলক নিয়ম লাগে, যার সব literal positive: “ক্রেতা প্রিমিয়াম” (p), বা “প্রতিটি অর্ডার অন্তত একটি স্লটে যাবে” (x₁ ∨ x₂ ∨ x₃)। তাই নিয়ম পর্যালোচনার সময় বাধ্যতামূলক নিয়মগুলোকে আলাদা চোখে দেখুন।

বাজারঘরের ডেলিভারি দলের নিয়ম, যেখানে u = “আজই ডেলিভারি”, c = “ক্যাশ অন ডেলিভারি”, h = “ঠিকানা হাওর এলাকায়”, p = “ক্রেতা প্রিমিয়াম সদস্য”:

• R1: হাওর এলাকায় আজই ডেলিভারি নয়: h → ¬u
• R2: প্রিমিয়াম সদস্য সবসময় আজই পান: p → u
• R3: প্রিমিয়াম সদস্যরা আগে টাকা দেন, ক্যাশ অন ডেলিভারি নয়: p → ¬c
• R4: হাওর এলাকায় শুধু ক্যাশ অন ডেলিভারি: h → c
• F1 আর F2 (একটি অর্ডারের ঘটনা): ঠিকানা হাওরে (h), ক্রেতা প্রিমিয়াম (p)

R1–R4-এর প্রতিটিতে negative literal আছে, তাই উপপাদ্য ২.১ অনুযায়ী এরা নিজেরা consistent. বিরোধ এলে আসবে F1, F2-এর মতো বাধ্যতামূলক তথ্য থেকে। কোন নিয়মগুলো একসঙ্গে বিরোধ ঘটায়, তা খুঁজতে সব উপসেট ছোট থেকে বড় ক্রমে পরীক্ষা করি। যে উপসেট নিজে unsatisfiable কিন্তু যার যেকোনো একটি নিয়ম বাদ দিলে satisfiable, তাকে বলে minimal unsat core.

from itertools import product, combinations

# u = আজই ডেলিভারি, c = ক্যাশ অন ডেলিভারি,
# h = ঠিকানা হাওর এলাকায়, p = ক্রেতা প্রিমিয়াম সদস্য
imp = lambda a, b: (not a) or b
rules = {
    "R1 h -> not u": lambda u, c, h, p: imp(h, not u),
    "R2 p -> u":     lambda u, c, h, p: imp(p, u),
    "R3 p -> not c": lambda u, c, h, p: imp(p, not c),
    "R4 h -> c":     lambda u, c, h, p: imp(h, c),
    "F1 h":          lambda u, c, h, p: h,
    "F2 p":          lambda u, c, h, p: p,
}

def models(names):
    return [row for row in product([True, False], repeat=4)
            if all(rules[n](*row) for n in names)]

print("all 6:", len(models(rules)), "assignments")
for k in range(1, 7):                  # ছোট থেকে বড় উপসেট
    cores = [g for g in combinations(rules, k) if not models(g)]
    if cores:
        print(f"smallest conflicting sets, size {k}:")
        for g in cores:
            print("  ", [n[:2] for n in g])
        break
for n in rules:                        # একটি করে বাদ দিয়ে দেখা
    rest = [m for m in rules if m != n]
    print(f"without {n[:2]}: {len(models(rest))} assignment(s)")

all 6: 0 assignments
smallest conflicting sets, size 4:
   ['R1', 'R2', 'F1', 'F2']
   ['R3', 'R4', 'F1', 'F2']
without R1: 0 assignment(s)
without R2: 0 assignment(s)
without R3: 0 assignment(s)
without R4: 0 assignment(s)
without F1: 1 assignment(s)
without F2: 1 assignment(s)

সফটওয়্যারের requirement সংগ্রহ আর পর্যালোচনার পুরো প্রক্রিয়া সফটওয়্যার ইঞ্জিনিয়ারিং ও Git কোর্সের পর্ব ২০-এ আছে। এখানে আমরা দেখলাম তার গাণিতিক কেন্দ্রটুকু: নিয়মকে সূত্রে লিখলে “পরস্পরবিরোধী কি না” প্রশ্নটি যন্ত্রকে দেওয়া যায়।

৩ · ধাঁধাকে clause-এ লেখা — Sudoku আর “ঠিক একটি”

Sudoku, n-queens, ক্লাসের রুটিন, ডেলিভারির স্লট: সবগুলোই constraint satisfaction সমস্যা। কিছু ঘরে মান বসাতে হবে, এমনভাবে যাতে সব শর্ত মানা হয়। এদের SAT-এ আনার কৌশলকে বলে SAT encoding: প্রতিটি “এই ঘরে এই মান কি না” প্রশ্নের জন্য একটি সত্য-মিথ্যা variable, আর প্রতিটি শর্তের জন্য কয়েকটি clause. ফলে পাওয়া যায় CNF সূত্র, যা যেকোনো SAT solver নেয়।

4 × 4 Sudoku নিই: প্রতিটি সারি, কলাম আর 2 × 2 বাক্সে 1–4 ঠিক একবার। Variable x_r,c,v মানে “সারি r, কলাম c-এর ঘরে v আছে”। r, c, v প্রতিটির ৪টি মান, তাই 4 × 4 × 4 = ৬৪টি variable. প্রতিটি নিয়মই “ঠিক একটি” ধরনের: প্রতিটি ঘরে ঠিক একটি সংখ্যা, প্রতিটি সারিতে প্রতিটি সংখ্যা ঠিক একবার, ইত্যাদি। একটি নিয়ম clause-এ লিখি:

1x1c = x(1,c,3)2অন্তত ১টি: x11 ∨ … ∨ x143বড়জোর ১টি: ¬x11 ∨ ¬x124… বাকি ৫টি জোড়া5মোট: ১ + ৬ = ৭

প্রমাণ (দুই দিক আলাদা করে):

1. (⇐) বড়জোর একটি সত্য হলে সব clause সত্য। যেকোনো জোড়া i < j নিন। বড়জোর একটি সত্য বলে x_i আর x_j দুটোই সত্য নয়; তাই অন্তত একটি মিথ্যা, ধরুন x_i. তখন ¬x_i = T, আর clause ¬x_i ∨ ¬x_j সত্য।
2. (⇒) সব clause সত্য হলে বড়জোর একটি সত্য। Contrapositive দিয়ে দেখাই: ধরুন দুটি বা বেশি সত্য, যেমন x_i = x_j = T, i < j. তখন clause ¬x_i ∨ ¬x_j = F ∨ F = F, অর্থাৎ অন্তত একটি clause মিথ্যা।
3. “ঠিক একটি” = “অন্তত একটি” ∧ “বড়জোর একটি”; প্রথমটি একটি clause, দ্বিতীয়টি ধাপ ১–২ অনুযায়ী C(n, 2)টি clause. মোট 1 + C(n, 2). ∎

C(n, 2) = n(n − 1)/2 দ্রুত বাড়ে: n = 100-এ ৪,৯৫০টি clause. তাই বড় গ্রুপে solver-রা অতিরিক্ত সাহায্যকারী variable দিয়ে প্রায় রৈখিক সংখ্যক clause-এর encoding ব্যবহার করে (যেমন sequential counter); অংশ ৫-এ PySAT-এ সেটি দেখবেন। Combination-এর গণনা পর্ব ৩৩-এ বিস্তারিত আসবে। নিচের ব্লক যেকোনো k-এর জন্য k² × k² Sudoku encode করে clause গোনে, আর একটি পূরণ করা গ্রিড সব clause মানে কি না যাচাই করে।

from itertools import combinations

def encode(k):                          # k = 2 → 4×4, k = 3 → 9×9
    n = k * k
    var = lambda r, c, v: n * n * r + n * c + v + 1
    groups = []
    for r in range(n):
        for c in range(n):
            groups.append([var(r, c, v) for v in range(n)])          # ঘর
    for v in range(n):
        for i in range(n):
            groups.append([var(i, c, v) for c in range(n)])          # সারি
            groups.append([var(r, i, v) for r in range(n)])          # কলাম
            br, bc = k * (i // k), k * (i % k)
            groups.append([var(br + a, bc + b, v)
                           for a in range(k) for b in range(k)])     # বাক্স
    cnf = []
    for g in groups:
        cnf.append(g)                                 # অন্তত একটি
        cnf += [[-a, -b] for a, b in combinations(g, 2)]   # বড়জোর একটি
    return n, var, cnf

for k in (2, 3, 4):
    n, var, cnf = encode(k)
    print(f"{n}x{n}: variables {n**3}, clauses {len(cnf)}")

n, var, cnf = encode(2)
grid = ["1234", "3412", "2143", "4321"]             # একটি পূরণ করা 4×4
true = {var(r, c, int(grid[r][c]) - 1) for r in range(4) for c in range(4)}
holds = lambda cl: any((l > 0) == (abs(l) in true) for l in cl)
print("valid grid satisfies all:", all(holds(cl) for cl in cnf))
grid[0] = "1243"                                    # এক সারিতে দুটি ঘর অদলবদল
true = {var(r, c, int(grid[r][c]) - 1) for r in range(4) for c in range(4)}
print("after a swap, violated clauses:", sum(not holds(cl) for cl in cnf))

4x4: variables 64, clauses 448
9x9: variables 729, clauses 11988
16x16: variables 4096, clauses 123904

valid grid satisfies all: True
after a swap, violated clauses: 4

পুরো প্রক্রিয়াটি এক ছবিতে: বাস্তব সমস্যা থেকে CNF, solver, তারপর দুই রকম উত্তর।

৪ · DPLL — বাধ্য মান ছড়ানো, অনুমান আর পিছিয়ে আসা

৭২৯টি variable-এর সব সারি দেখা অসম্ভব: 2⁷²⁹ একটি ২২০ অঙ্কের সংখ্যা। Solver তাহলে কী করে? ভিত্তিটি DPLL পদ্ধতি, যার নাম Davis, Putnam, Logemann আর Loveland-এর নামের আদ্যক্ষর থেকে। তিনটি ধারণা:

• সরল করা: একটি literal ℓ সত্য ধরলে যে clause-এ ℓ আছে সেটি সত্য হয়ে বাদ যায়, আর যে clause-এ ¬ℓ আছে সেখান থেকে ¬ℓ মুছে যায় (সেটি আর সাহায্য করতে পারবে না)। ফলের সূত্রকে লেখা হয় F|ℓ.
• Unit propagation: কোনো clause-এ একটিই literal বাকি থাকলে (unit clause) তার মান বাধ্য, অনুমানের দরকার নেই। একটি বাধ্য মান অন্য clause-কে unit বানায়, সেখান থেকে আরেকটি: শিকলের মতো ছড়ায়।
• শাখা আর backtracking: বাধ্য মান না থাকলে একটি variable বেছে T ধরে এগোন; কোনো clause-এর সব literal মুছে গেলে (empty clause) বিরোধ, তখন পিছিয়ে এসে F চেষ্টা করুন।

নিচের পাঁচটি clause-এর সূত্রে DPLL হাতে চালাই (a, b, c, d চারটি variable):

(a ∨ b) ∧ (¬a ∨ c) ∧ (¬c ∨ d) ∧ (¬b ∨ ¬d) ∧ (¬a ∨ ¬d)

C1a ∨ bC2¬a ∨ cC3¬c ∨ dC4¬b ∨ ¬dC5¬a ∨ ¬d

এবার পদ্ধতিটি কেন সঠিক, তার প্রমাণ। এখানে F একটি CNF সূত্র, আর “F satisfiable” মানে কোনো মান-বসানোয় F-এর সব clause সত্য।

প্রমাণ:

1. (ক) F-এর যেকোনো model-এ x হয় T নয় F. x = T হলে: যে clause-এ x আছে তা সত্য, আর যে clause-এ ¬x আছে তার সত্যতা আসে অন্য কোনো literal থেকে (¬x মিথ্যা); তাই একই মান-বসানো F|x-এর প্রতিটি clause সত্য করে। x = F হলে একইভাবে F|¬x. উল্টো দিকে, F|x-এর একটি model নিয়ে তাতে x = T যোগ করলে মুছে-ফেলা clause-গুলো (x আছে বলে) আর ছোট-করা clause-গুলো (বাকি অংশ সত্য বলে) সবই সত্য, তাই F সত্য; F|¬x-এর ক্ষেত্রেও একই যুক্তি।
2. (খ) F-এর যেকোনো model-এ unit clause (ℓ) সত্য, অর্থাৎ ℓ = T. তাই (ক)-এর দুই শাখার মধ্যে ¬ℓ শাখায় কোনো model নেই, আর F satisfiable ⇔ F|ℓ satisfiable.
3. (গ) Empty clause-এ কোনো literal নেই, তাই কোনো মান-বসানোয় তা সত্য হতে পারে না; ∧-এ একটি মিথ্যা থাকলে পুরো F মিথ্যা। ∎

প্রমাণ (খোলা variable-এর সংখ্যা k-এর ওপর strong induction; পূর্ণ নিয়ম পর্ব ১১-এ):

1. ভিত্তি, k = 0: কোনো variable বাকি নেই, তাই প্রতিটি clause হয় সব literal মুছে empty, নয় আগেই সত্য হয়ে বাদ। Empty clause থাকলে DPLL UNSAT বলে, Lemma (গ) অনুযায়ী ঠিক; না থাকলে সূত্র খালি, সব clause সত্য, DPLL SAT বলে: ঠিক।
2. ধরে নিই: k-এর চেয়ে কম খোলা variable-এর সব সূত্রে দাবিটি সত্য।
3. ধাপ: k খোলা variable-এ DPLL হয় একটি unit ℓ বসায়, নয় x-এ শাখা করে। প্রতিটি ক্ষেত্রে নতুন সূত্রে খোলা variable অন্তত একটি কমে, তাই induction-এর অনুমান খাটে: প্রতিটি পুনরাবৃত্ত ডাক থামে আর সঠিক উত্তর দেয়।
4. Unit-এর ক্ষেত্রে Lemma (খ) বলে F আর F|ℓ একসঙ্গে satisfiable বা unsatisfiable, তাই উত্তর ঠিক। শাখার ক্ষেত্রে DPLL প্রথমে F|x, ব্যর্থ হলে F|¬x চেষ্টা করে; Lemma (ক) বলে F satisfiable ঠিক তখন, যখন দুটির অন্তত একটি satisfiable. তাই দুটোই ব্যর্থ হলে UNSAT ঠিক, আর কোনো একটি SAT হলে তার model-এ শাখার literal যোগ করে F-এর model পাওয়া যায়। ∎

প্রমাণটি খরচ নিয়ে কিছু বলে না: খারাপ ক্ষেত্রে শাখার গাছে প্রায় 2ⁿটি পাতা থাকতে পারে। নিচের ব্লকে উপরের stepper-এর হুবহু DPLL, প্রতিটি সিদ্ধান্ত ছাপাসহ। দ্বিতীয় ডাকে একটি ষষ্ঠ clause (a ∨ ¬b) যোগ করা হয়েছে; দেখুন কী হয়। Literal লেখা হয়েছে সংখ্যায়, যেমন SAT solver-দের প্রচলিত DIMACS রীতিতে: 1 = a, −1 = ¬a.

def simplify(cnf, lit):                 # lit সত্য ধরে সূত্র ছোট করা
    out = []
    for cl in cnf:
        if lit in cl:
            continue                    # clause সত্য হয়ে গেছে, বাদ
        out.append([l for l in cl if l != -lit])   # মিথ্যা literal মুছে ফেলা
    return out

def dpll(cnf, assign, depth=0):
    pad = "  " * depth
    while True:                         # unit propagation
        if [] in cnf:
            print(pad + "conflict: empty clause, back")
            return None
        units = [cl[0] for cl in cnf if len(cl) == 1]
        if not units:
            break
        u = units[0]
        print(pad + f"unit {u:+d}")
        assign, cnf = assign + [u], simplify(cnf, u)
    if not cnf:
        return assign                   # সব clause সত্য
    x = abs(cnf[0][0])                  # শাখা: প্রথম খোলা variable
    for lit in (x, -x):
        print(pad + f"decide {lit:+d}")
        res = dpll(simplify(cnf, lit), assign + [lit], depth + 1)
        if res is not None:
            return res
    return None

# 1=a, 2=b, 3=c, 4=d;  -1 মানে ¬a
F = [[1, 2], [-1, 3], [-3, 4], [-2, -4], [-1, -4]]
for formula in (F, F + [[1, -2]]):
    res = dpll(formula, [])
    print("result:", res if res is not None else "UNSAT", "\n")

decide +1
  unit +3
  unit +4
  conflict: empty clause, back
decide -1
  unit +2
  unit -4
  unit -3
result: [-1, 2, -4, -3]

decide +1
  unit +3
  unit +4
  conflict: empty clause, back
decide -1
  unit +2
  conflict: empty clause, back
result: UNSAT

৫ · আসল SAT solver — CDCL, PySAT দিয়ে Sudoku আর ডেলিভারি স্লট

আধুনিক SAT solver DPLL-এর কাঠামো রাখে, কিন্তু একটি বড় কৌশল যোগ করে: CDCL (conflict-driven clause learning). প্রতিবার বিরোধ হলে solver খুঁজে দেখে কোন অনুমানগুলো মিলে বিরোধটি ঘটাল, তারপর “এই অনুমানগুলো একসঙ্গে চলবে না” কথাটি একটি নতুন clause হিসেবে সূত্রে যোগ করে, আর দরকার হলে অনেক ধাপ পেছনে এক লাফে ফেরে। উপরের stepper-এ বিরোধের কারণ ছিল শুধু a = T; CDCL সেখান থেকে শিখত clause (¬a), যা আর কখনো ভুলবে না। নতুন clause মূল সূত্রের যৌক্তিক ফল (পর্ব ০৬-এর resolution দিয়ে পাওয়া), তাই যোগ করলে সমাধানের সেট বদলায় না।

সত্যিকারের run ১: 9 × 9 Sudoku

নিচের পরীক্ষাগুলো এই কোর্সের লেখার সময় একটি সাধারণ Windows ডেস্কটপে সত্যিকারভাবে চালানো হয়েছে: Python 3.12, python-sat 1.9.dev21 (PySAT, MIT লাইসেন্স; ভেতরে Armin Biere-এর CaDiCaL 1.9.5 solver, এটিও MIT) আর z3-solver 5.3.3 (MIT). নিজের কম্পিউটারে চালাতে চাইলে:

cd ~/bazarghar-dm
uv add python-sat z3-solver
uv run python sudoku_sat.py hard

ফাইলের মূল অংশ, অংশ ৩-এর encoding-ই, শুধু 9 × 9-এ (পুরো ফাইলে আরও আছে ধাঁধার স্ট্রিং আর গ্রিড ছাপার কয়েক লাইন):

from pysat.solvers import Solver

def var(r, c, v):              # r, c, v in 0..8  ->  1..729
    return 81 * r + 9 * c + v + 1

def exactly_one(lits):
    yield list(lits)                                   # at least one
    for a, b in combinations(lits, 2):                 # at most one
        yield [-a, -b]
# … cell, row, column, box groups → cnf (11988 clauses) …
givens = [[var(k // 9, k % 9, int(ch) - 1)] for k, ch in enumerate(P) if ch != "."]
cnf += givens

with Solver(name="cadical195", bootstrap_with=cnf) as s:
    t0 = time.perf_counter(); ok = s.solve(); t1 = time.perf_counter()
    model = set(l for l in s.get_model() if l > 0)
    # … print the grid …
    s.add_clause([-l for l in model if l <= 729])      # block this solution
    again = s.solve()                                  # a second solution?

সত্যিকারের run-এর আউটপুট, মাত্র ২১টি দেওয়া ঘরের একটি ধাঁধায় (হাতে করতে গেলে অনেক অনুমান লাগে, এমন ধরনের):

$ uv run python sudoku_sat.py hard
variables: 729, rule clauses: 11988, givens: 21, total: 12009
SAT in 0.7 ms
8 1 2 7 5 3 6 4 9
9 4 3 6 8 2 1 7 5
6 7 5 4 9 1 2 8 3
1 5 4 2 3 7 8 9 6
3 6 9 8 4 5 7 2 1
2 8 7 1 6 9 5 3 4
5 2 1 9 7 4 3 6 8
4 3 8 5 2 6 9 1 7
7 9 6 3 1 8 4 5 2
another solution? False (0.1 ms)  -> unique
solver stats: {'decisions': 84, 'conflicts': 79, 'propagations': 5994}

তিনটি জিনিস লক্ষ করুন। প্রথমত, সময় এক মিলিসেকেন্ডেরও কম; মানুষের কাছে যা কঠিন, solver-এর কাছে তা ছোট। দ্বিতীয়ত, blocking clause: পাওয়া উত্তরের ঠিক বিপরীত একটি clause যোগ করে আবার চালালে UNSAT এলো, অর্থাৎ উত্তরটি অনন্য; এভাবে solver-কে “আর কোনো সমাধান আছে কি?” প্রশ্নও করা যায়। তৃতীয়ত, পরিসংখ্যান: ৮৪টি অনুমান আর ৭৯টি বিরোধ, অথচ প্রায় ছয় হাজার বাধ্য মান-ছড়ানো; কাজের বেশিরভাগ করেছে unit propagation. (একই ফাইলে সহজ, ৩০ ঘরের একটি ধাঁধায় solver একটিও অনুমান না করে শুধু propagation-এ মিলিয়েছে।) সময়ের সংখ্যা যন্ত্রভেদে বদলাবে।

সত্যিকারের run ২: বাজারঘরের ডেলিভারি স্লট

একটি ভ্যান, তিনটি স্লট (সকাল, দুপুর, বিকেল), ছয়টি ডেলিভারি D1–D6. নিয়ম: প্রতিটি ডেলিভারি ঠিক একটি স্লটে; প্রতি স্লটে বড়জোর ২টি; D1 আর D4 শহরের দুই প্রান্তে, D2 আর D3-ও, তাই এই জোড়াগুলো একই স্লটে নয়; D3 শুধু সকাল বা দুপুর; D5 সকালে নয়; D6 শুধু বিকেলে। “বড়জোর ২টি” একটি cardinality constraint; PySAT তাকে sequential counter নামের encoding-এ কিছু সাহায্যকারী variable দিয়ে clause বানায়।

for s in S:                                        # one van: at most 2 per slot
    enc = CardEnc.atmost([x(d, s) for d in D], bound=2,
                         vpool=pool, encoding=EncType.seqcounter)
    hard += enc.clauses
# … exactly-one slot per delivery, far-apart pairs, customer wishes …

# new requests, each switched on by an "assumption" literal
req = {"R1 D2 evening only": [x("D2", "evening")],
       "R2 D4 evening only": [x("D4", "evening")],
       "R3 D1 not noon":     [-x("D1", "noon")],
       "R4 D5 noon only":    [x("D5", "noon")]}
# … add (not sel or request) for each, then:
s.solve(assumptions=list(sel.values()))
core = s.get_core()

$ uv run python slots_sat.py
variables: 42 (18 slot vars + 24 counter vars), clauses: 87
a schedule: {'D1': 'morning', 'D2': 'morning', 'D3': 'noon', 'D4': 'noon', 'D5': 'evening', 'D6': 'evening'}
all schedules: 10
with all 4 requests: UNSAT
conflicting requests: ['R1 D2 evening only', 'R2 D4 evening only']

Solver একটি সময়সূচি দিল, আর blocking clause দিয়ে সব গুনে বলল মোট ১০টি বৈধ সময়সূচি (আলাদা একটি brute-force স্ক্রিপ্ট 3⁶ = ৭২৯টি বিন্যাস ঘুরে একই ১০ পেয়েছে)। এরপর ক্রেতাদের চারটি নতুন অনুরোধ এলো। প্রতিটি অনুরোধের সঙ্গে একটি “সুইচ” variable জুড়ে দিয়ে solver-কে বলা হলো সব সুইচ চালু ধরে চেষ্টা করতে (assumption). উত্তর UNSAT, আর core বলছে দোষী শুধু R1 আর R2: D6 আগেই বিকেলে বাঁধা, R1 আর R2 আরও দুটি ডেলিভারি বিকেলে চায়, অথচ ভ্যানে জায়গা দুটি। R3 আর R4 নির্দোষ। অংশ ২-এর brute-force core খোঁজা এখানে solver-এর ভেতরেই হলো, আর এই পদ্ধতি হাজারো নিয়মেও চলে।

৬ · SMT আর Z3 — টাকার অঙ্কওয়ালা নিয়ম যাচাই

বাস্তবের নিয়মে শুধু সত্য-মিথ্যা থাকে না; থাকে “অর্ডার ৩০০ টাকার বেশি”, “ছাড় মোটের ২০%-এর বেশি নয়”। এগুলোকে bit-এ ভেঙে SAT-এ লেখা যায়, কিন্তু ঝামেলার। SMT solver (satisfiability modulo theories) সরাসরি এমন সূত্র নেয়, যেখানে Boolean variable-এর পাশাপাশি পূর্ণসংখ্যা, বাস্তব সংখ্যা, array আর bit-vector-এর ওপর শর্ত থাকে। ভেতরে একটি SAT solver যুক্তির কাঠামো সামলায়, আর প্রতিটি “তত্ত্বের” আলাদা অংশ (যেমন রৈখিক অসমতার সমাধানকারী) বলে সংখ্যার শর্তগুলো একসঙ্গে সম্ভব কি না। সবচেয়ে পরিচিত বিনামূল্যের SMT solver-গুলোর একটি Z3; ২০০৮ সালের একটি গবেষণাপত্রে Leonardo de Moura আর Nikolaj Bjørner এটি পরিচয় করিয়ে দেন, আর পরে এটি MIT লাইসেন্সে উন্মুক্ত হয়।

সত্যিকারের run ৩: সরল করা শর্ত সব পূর্ণসংখ্যায় প্রমাণ

অংশ ১-এ Python ৮টি সারি দেখেছিল, যেখানে b একটি সত্য-মিথ্যা variable. আসল কোডে total একটি পূর্ণসংখ্যা। Z3-কে সরাসরি জিজ্ঞেস করি: সব সম্ভাব্য total-এ দুটি শর্ত কি সমান?

from z3 import Bools, Int, Not, And, Or, prove

member, remote = Bools("member remote")
total = Int("total")

messy = And(Not(And(Not(member), total < 1000)), Not(And(remote, Not(member))))
clean = Or(member, And(total >= 1000, Not(remote)))
wrong = And(member, total >= 1000, Not(And(remote, Not(member))))

print("messy == clean :", end=" "); prove(messy == clean)
print("messy == wrong :", end=" "); prove(messy == wrong)

$ uv run python cond_z3.py
messy == clean : proved
messy == wrong : counterexample
[remote = True, member = True, total = 0]

prove(G) ভেতরে কী করে? ¬G satisfiable কি না দেখে। ¬G-এর কোনো model না থাকলে G সব ক্ষেত্রে সত্য, অর্থাৎ tautology (অনুশীলন ১-এ এর প্রমাণ)। থাকলে সেই model-ই একটি counterexample: দূরের জেলার একজন সদস্য, ০ টাকার অর্ডার; মূল শর্তে তিনি ফ্রি ডেলিভারি পান, ভুল রূপে পান না। ৮ সারির পরীক্ষার চেয়ে এটি শক্তিশালী: total-এর অসীম সংখ্যক মানের জন্য একবারে প্রমাণ।

সত্যিকারের run ৪: কুপন-নিয়মে ফাঁক খোঁজা

বাজারঘরের কুপন-নিয়ম, যেখানে total = অর্ডারের মোট টাকা, disc = ছাড়ের টাকা:

• S1: ছাড় কখনো ঋণাত্মক নয়: disc ≥ 0
• S2: ছাড় মোটের ২০%-এর বেশি নয়: 5 · disc ≤ total
• S3: নতুন ক্রেতা আর মোট ≥ ৩০০ হলে ছাড় অন্তত ১০০ টাকা
• S4: মোট ৩০০-এর কম হলে কোনো ছাড় নেই: disc = 0

from z3 import Int, Bool, Solver, Implies, And, Not, ForAll

total, disc = Int("total"), Int("disc")      # order total and discount, in taka
new = Bool("new_customer")
rules = {
    "S1 discount is never negative":          disc >= 0,
    "S2 discount at most 20% of total":       5 * disc <= total,
    "S3 new customer, total >= 300 -> >=100": Implies(And(new, total >= 300), disc >= 100),
    "S4 total < 300 -> no discount":          Implies(total < 300, disc == 0),
}
s = Solver(); s.add(*rules.values())
print("1) all rules together:", s.check(), "->", s.model())

s = Solver()                                 # an order with NO legal discount?
s.add(total >= 0, ForAll([disc], Not(And(*rules.values()))))
print("2) order with no legal discount:", s.check(), "->", s.model())

s = Solver(); s.set(unsat_core=True)         # which rules clash at 400 taka?
for name, r in rules.items():
    s.assert_and_track(r, name)
s.add(total == 400, new)
print("3) new customer, 400 taka:", s.check(), "-> core", s.unsat_core())

$ uv run python coupon_z3.py
1) all rules together: sat -> [new_customer = True, disc = 100, total = 500]
2) order with no legal discount: sat -> [new_customer = True, total = 304]
3) new customer, 400 taka: unsat -> core [S2 discount at most 20% of total,
 S3 new customer, total >= 300 -> >=100]

প্রথম প্রশ্নে নিয়মগুলো consistent: ৫০০ টাকার অর্ডারে নতুন ক্রেতা ১০০ টাকা ছাড় পেলে সব মানা হয়। কিন্তু consistent মানেই নির্ভুল নয়। দ্বিতীয় প্রশ্নটি nested quantifier (পর্ব ০৫): “এমন কোনো total আছে কি, যার জন্য প্রতিটি disc-এ কোনো না কোনো নিয়ম ভাঙে?” Z3 একটি পেল: ৩০৪ টাকার অর্ডারে নতুন ক্রেতা। S3 বলে ছাড় ≥ ১০০, S2 বলে ছাড় ≤ ৩০৪/৫, অর্থাৎ ≤ ৬০. হাতে হিসাব করলে ফাঁকটি পুরো পরিসর: ৩০০ ≤ total < ৫০০, কারণ 5 × 100 = 500. তৃতীয় প্রশ্নে ৪০০ টাকার অর্ডারে Z3-এর unsat core দোষী হিসেবে দেখাল ঠিক S2 আর S3. চেকআউট কোড লেখার আগেই নীতিনির্ধারকদের জানানো যায়: “৩০০ থেকে ৪৯৯ টাকার অর্ডারে নতুন ক্রেতার জন্য আপনার দুটি নিয়ম একসঙ্গে মানা অসম্ভব।”

৭ · SAT আর NP-completeness — কেন কঠিন, তবু কেন চলে

অংশ ৩-এ দেখেছেন: একটি প্রস্তাবিত মান-বসানো দিলে সব clause একবার করে দেখে polynomial সময়ে যাচাই করা যায়। এমন “দ্রুত যাচাইযোগ্য” সমস্যার শ্রেণির নাম NP. SAT এই শ্রেণির একটি বিশেষ সদস্য:

এটি সাধারণত Stephen Cook-এর ১৯৭১ সালের প্রবন্ধের নামে পরিচিত; Leonid Levin প্রায় একই সময়ে সোভিয়েত ইউনিয়নে স্বাধীনভাবে একই ধরনের ফল পান (Cook–Levin theorem). প্রমাণের মূল ভাবনা: যেকোনো যাচাই-প্রোগ্রামের ধাপে ধাপে চলাকে বিশাল একটি clause-এর তালিকায় লেখা যায়, ঠিক যেমন আমরা Sudoku-র নিয়ম লিখেছি। এই পর্বের Sudoku, সময়সূচি আর পর্ব ৬৩-এর graph coloring একই কৌশলে SAT-এ যায়। পুরো প্রমাণ আর reduction-এর ধারণা DSA কোর্সের পর্ব ৬৪-এ।

তাই দুটি কথা একসঙ্গে সত্য। তাত্ত্বিকভাবে: সব ক্ষেত্রে polynomial সময়ে SAT সমাধানের কোনো পদ্ধতি জানা নেই, আর থাকলে P = NP হতো, যা কম্পিউটার বিজ্ঞানের সবচেয়ে বিখ্যাত খোলা প্রশ্ন। ছোট আকারের কিছু ধরন অবশ্য সহজ: প্রতিটি clause-এ বড়জোর দুটি literal থাকলে (2-SAT) polynomial সময়ের পদ্ধতি আছে, কিন্তু তিনটি হলেই (3-SAT) সমস্যা আবার NP-complete. ব্যবহারিকভাবে: chip নকশা যাচাই, সফটওয়্যার পরীক্ষা, সময়সূচি আর package-এর নির্ভরতা মেলানোর মতো কাজে লাখো variable-এর সূত্র প্রায়ই দ্রুত মেলে, কারণ বাস্তবের সূত্রে গঠন থাকে আর CDCL সেই গঠন কাজে লাগায়। খারাপ ক্ষেত্রও বানানো যায়, তাই সময়সীমা রাখতে হয়।

৮ · AI-এর যুগে — শর্ত, নিয়ম আর encoding-এ AI সহকারী

AI সহকারী একটি জটিল if-শর্ত “সরল” করে দিতে, নিয়মের তালিকা থেকে Z3 কোড লিখে দিতে বা Sudoku-র encoding বানাতে খুব দ্রুত। কিন্তু এখানে তার ভুল বিশেষভাবে বিপজ্জনক: ভুল encoding-এ solver নির্ভুলভাবে ভুল প্রশ্নের উত্তর দেয়, আর “SAT” বা “proved” লেখা দেখে সবাই নিশ্চিন্ত হয়ে যান। এই বিষয়ে যে ভুলগুলো বেশি দেখা যায়:

AI-এর উত্তর হাতে পেলে — যাচাইয়ের চেকলিস্ট

• সরল করা শর্ত সব সারিতে (বা Z3-এ সব পূর্ণসংখ্যায়) মূল শর্তের সমান কি না যাচাই করেছি
• সীমানার মান আর None/শূন্যের মতো বিশেষ ক্ষেত্র আলাদা করে চালিয়ে দেখেছি
• ছোট আকারে (যেমন 4 × 4) variable আর clause গুনে সূত্রের সঙ্গে মিলিয়েছি
• Solver-এর দেওয়া model মূল নিয়মে আলাদা কোডে যাচাই করেছি, শুধু “SAT” লেখায় ভরসা করিনি
• UNSAT হলে core দেখে বুঝেছি কোন নিয়মগুলো বিরোধী, আর সেটি হাতেও বুঝিয়ে বলতে পারি
• উল্লেখ করা উপপাদ্যের শর্ত (যেমন “2-SAT polynomial” কিন্তু 3-SAT নয়) আর উৎস নিজে একটি বিশ্বস্ত বইয়ে মিলিয়েছি

AI-তে যুক্তি আর constraint কীভাবে ব্যবহার হয়, তা AI-এর ভিত্তি আর Python for AI কোর্সের পর্ব ৪৩ (constraint satisfaction) আর পর্ব ৪৫-এ আছে; এখানে আমরা তার নিচের গণিত আর যাচাইয়ের দিকটি দেখলাম।