Propositional logic — বাক্য, truth table আর inference

মডিউল ৭ জুড়ে (পর্ব ৩৯ থেকে পর্ব ৪৪) agent শিখেছে পথ খুঁজতে আর নিয়ম মেনে মান বসাতে। কিন্তু সেখানে নিয়মগুলো কোডের ভেতরে লুকানো ছিল। এই মডিউলে প্রশ্নটি অন্য: জ্ঞানকে কি এমন ভাষায় লেখা যায়, যা থেকে যন্ত্র নিজেই নতুন সিদ্ধান্ত টেনে বের করে, আর প্রতিটি সিদ্ধান্তের পক্ষে প্রমাণও দেখায়? সবচেয়ে সরল সেই ভাষা propositional logic. এখানের সব নিয়ম কাল্পনিক অনলাইন দোকান বাজারঘরের, বানানো।

১ · Knowledge-based agent — KB, TELL আর ASK

বাজারঘরের কাস্টমার-সাপোর্টে নতুন একজন কর্মী যোগ দিয়েছেন। প্রথম দিন তাঁকে একটি খাতা দেওয়া হলো, যাতে দোকানের নিয়ম লেখা: “অর্ডার ৳১,০০০-এর বেশি হলে delivery ফ্রি”, “ফ্রি delivery আর ঢাকার ঠিকানা হলে একই দিনে পৌঁছায়”, “pre-order পণ্য একই দিনে যায় না”। কাস্টমার ফোন করে জিজ্ঞেস করেন, “আমার ৳১,২০০-র অর্ডার, ঠিকানা মিরপুর, আজই পাব?” কর্মী খাতা দেখে, নিয়মগুলো জুড়ে উত্তর দেন। কোনো নিয়মে সরাসরি “৳১,২০০ আর মিরপুর হলে আজই” লেখা নেই; উত্তরটি বের করে আনা হয়েছে।

Russell ও Norvig-এর পাঠ্যবই “Artificial Intelligence: A Modern Approach” এই ধরনের agent-কে দুটি কাজ দিয়ে বর্ণনা করে:

• TELL(KB, বাক্য): নতুন একটি কথা knowledge base-এ যোগ করা। শুরুতে নিয়ম, পরে প্রতিটি নতুন তথ্য (“এই অর্ডার ৳১,২০০-র”)।
• ASK(KB, প্রশ্ন): জিজ্ঞেস করা, প্রশ্নের কথাটি KB থেকে নিশ্চিতভাবে বেরিয়ে আসে কি না। উত্তর “হ্যাঁ”, “না”, অথবা “জানা যায় না”।

এখানে দুটি অংশ আলাদা থাকে: জ্ঞান (KB-র বাক্যগুলো) আর যুক্তির যন্ত্র (inference engine). নতুন নিয়ম এলে কোড বদলাতে হয় না, শুধু TELL. এই আলাদা রাখার ধারণা John McCarthy-র ১৯৫৮ সালের দিকের “Programs with Common Sense” প্রবন্ধের “advice taker”-এর সঙ্গে সাধারণত যুক্ত করা হয়। পর্ব ৩-এ যে নিয়মভিত্তিক বা symbolic AI-এর কথা এসেছিল, তার গাণিতিক ভিত্তি এই পর্ব।

২ · বাক্য আর connective — ¬ ∧ ∨ → ↔ আর truth table

Propositional logic-এর সবচেয়ে ছোট একক একটি proposition: এমন একটি কথা, যা হয় সত্য (True, T) নয়তো মিথ্যা (False, F), মাঝামাঝি নয়। প্রতিটিকে একটি অক্ষর দিয়ে লেখা হয়, যাকে বলে proposition symbol বা atomic sentence. বাজারঘরের পাঁচটি symbol সারা পর্বে চলবে:

ছোট বাক্য জুড়ে বড় বাক্য বানাতে পাঁচটি connective:

• ¬ (not, না): negation. ¬P মানে “pre-order নয়”। P সত্য হলে ¬P মিথ্যা, উল্টোটাও।
• ∧ (and, এবং): conjunction. F ∧ D সত্য শুধু তখন, যখন দুটিই সত্য।
• ∨ (or, অথবা): disjunction. অন্তত একটি সত্য হলেই সত্য; দুটিই সত্য হলেও (inclusive or).
• → (implies, যদি … তাহলে): implication. B → F পড়ুন “B হলে F”. বাঁ দিক premise, ডান দিক conclusion.
• ↔ (if and only if, ঠিক তখনই): biconditional. দুই দিকের মান এক হলে সত্য।

প্রতিটি connective-এর পুরো অর্থ একটি truth table-এ ধরা যায়: দুটি symbol-এর চারটি সম্ভাব্য মান-মিশ্রণ, প্রতিটিতে ফল।

“যদি … তাহলে” কেন premise মিথ্যা হলে সত্য

A → B কলামটিই নতুনদের সবচেয়ে বেশি অবাক করে: A মিথ্যা হলে B যা-ই হোক, ফল সত্য। বাজারঘরের নিয়মটি দিয়ে ভাবুন: “অর্ডার ৳১,০০০-এর বেশি হলে delivery ফ্রি” (B → F). এটি একটি প্রতিশ্রুতি। প্রতিশ্রুতি কখন ভাঙল? শুধু তখন, যখন অর্ডার বড় ছিল অথচ delivery-র টাকা কাটা হলো। কেউ ৳৬০০-র অর্ডার দিলেন আর ঈদের অফারে ফ্রি delivery পেলেন: দোকান কি তার নিয়ম ভাঙল? না। নিয়মটি ছোট অর্ডার নিয়ে কিছুই বলেনি। নিচের stepper সারি ধরে ধরে টেবিলটি বানায়, পাশে আরও দুটি বাক্য রেখে: ¬F → ¬B (“ফ্রি না হলে অর্ডার বড় নয়”) আর F → B (“ফ্রি হলে অর্ডার বড়”)।

1for B, F in TT TF FT FF:2  B->F   = not B or F3  ~F->~B = F or not B4  F->B   = not F or B5compare columns

সংক্ষেপে, A → B আসলে ¬A ∨ B-এর সমান। এই রূপটিকে বলে material implication. দৈনন্দিন ভাষার “যদি”-তে প্রায়ই কারণ-ফলের ইঙ্গিত থাকে (“বৃষ্টি হলে রাস্তা ভেজে”), যুক্তিবিদ্যার → তা দাবি করে না। “২ + ২ = ৫ হলে ঢাকা বাংলাদেশের রাজধানী” যুক্তিবিদ্যায় সত্য বাক্য, যদিও শুনতে অদ্ভুত (ভাবনার প্রশ্ন ১)।

৩ · Syntax, semantics আর model — satisfiable, valid, equivalent

যুক্তিবিদ্যার একটি ভাষার দুটি দিক আছে। Syntax বলে কোন চিহ্নের সারি একটি বৈধ বাক্য: (B ∧ D) → S বৈধ, B ∧ → S নয়। এটি ব্যাকরণ, অর্থ নয়। Semantics বলে একটি বাক্য কোন অবস্থায় সত্য। এর মূল শব্দটি model: প্রতিটি symbol-এ একটি করে T বা F বসানো একটি সম্ভাব্য জগৎ। পাঁচটি symbol-এ 2⁵ = ৩২টি model; truth table-এর প্রতিটি সারি একটি model. (Machine learning-এর “model” শব্দের সঙ্গে গুলিয়ে ফেলবেন না; এখানে মানে “একটি সম্ভাব্য জগৎ”।)

কোনো model-এ বাক্য α সত্য হলে বলা হয় সেই model α-কে satisfy করে। সব model ঘুরে একটি বাক্যকে তিন ভাগে ফেলা যায়:

দুটি বাক্য α আর β logically equivalent (লেখা হয় α ≡ β) যদি প্রতিটি model-এ তাদের মান এক হয়; অন্যভাবে, α ↔ β valid. নিচের কোড এই সব সংজ্ঞা সরাসরি Python-এ লেখে: একটি বাক্য মানে একটি Python function, যা symbol-গুলোর True/False নিয়ে ফল দেয়; itertools.product সব model বানায়। প্রথমবার চালালে ব্রাউজারে Python নামতে কয়েক সেকেন্ড লাগতে পারে।

from itertools import product
imp = lambda a, b: (not a) or b          # a -> b
iff = lambda a, b: a == b                # a <-> b
TF = lambda v: "T" if v else "F"

def rows(f, names):                      # every model = one row
    return [(v, f(*v)) for v in product([True, False], repeat=len(names))]

def show(f, names, label):
    print(label)
    for v, r in rows(f, names):
        print("  ", " ".join(TF(x) for x in v), "|", TF(r))

def classify(f, names):
    res = [r for _, r in rows(f, names)]
    if all(res): return "valid (tautology)"
    return "satisfiable, not valid" if any(res) else "unsatisfiable"

def equivalent(f, g, names):             # same value in every model
    return classify(lambda *v: iff(f(*v), g(*v)), names).startswith("valid")

show(lambda B, F: imp(B, F), "BF", "B F | B -> F")
for label, f, n in [("P or not P", lambda P: P or not P, "P"),
                    ("P and not P", lambda P: P and not P, "P"),
                    ("B -> F", lambda B, F: imp(B, F), "BF"),
                    ("(B -> F) and B and not F",
                     lambda B, F: imp(B, F) and B and not F, "BF")]:
    print(f"{label:26}", classify(f, n))
pairs = {"De Morgan": (lambda A, B: not (A and B), lambda A, B: (not A) or (not B), "AB"),
         "contraposition": (lambda A, B: imp(A, B), lambda A, B: imp(not B, not A), "AB"),
         "converse": (lambda A, B: imp(A, B), lambda A, B: imp(B, A), "AB"),
         "distribution": (lambda A, B, C: A or (B and C),
                          lambda A, B, C: (A or B) and (A or C), "ABC")}
for name, (f, g, n) in pairs.items():
    print(f"{name:15}", "equivalent" if equivalent(f, g, n) else "NOT equivalent")

B F | B -> F
   T T | T
   T F | F
   F T | T
   F F | T
P or not P                 valid (tautology)
P and not P                unsatisfiable
B -> F                     satisfiable, not valid
(B -> F) and B and not F   unsatisfiable
De Morgan       equivalent
contraposition  equivalent
converse        NOT equivalent
distribution    equivalent

এই হিসাব Computer Fundamentals কোর্সের Boolean algebra পর্বের সঙ্গে একই গণিত: সেখানে AND, OR, NOT দিয়ে circuit সরল করা হয়, আর Computer Architecture কোর্সে সেই রাশিই logic gate হয়ে চিপে বসে। পার্থক্য উদ্দেশ্যে: circuit-এ লক্ষ্য একটি রাশি হিসাব করা, AI-তে লক্ষ্য রাশিগুলো থেকে কী বেরিয়ে আসে তা জানা।

৪ · Entailment আর model checking — KB ⊨ α

বাজারঘরের knowledge base-এ তিনটি নিয়ম:

• R1: B → F (অর্ডার ৳১,০০০-এর বেশি হলে delivery ফ্রি)
• R2: (F ∧ D) → S (ফ্রি delivery আর ঢাকার ঠিকানা হলে একই দিনে)
• R3: P → ¬S (pre-order হলে একই দিনে নয়)

এখন সংজ্ঞাটি: KB ⊨ α (পড়ুন “KB entails α”, চিহ্ন ⊨) মানে যে প্রতিটি model-এ KB-র সব বাক্য সত্য, সেখানে α-ও সত্য। একে বলে entailment. লিখে বললে: M(KB) ⊆ M(α), যেখানে M(x) মানে x যেসব model-এ সত্য তাদের সেট। লক্ষ করুন, KB-র বাক্য যত বেশি, M(KB) তত ছোট: প্রতিটি নতুন তথ্য কিছু সম্ভাব্য জগৎ বাদ দেয়।

সংজ্ঞাটিই একটি অ্যালগরিদম: সব model একে একে বানান, যেখানে KB সত্য সেখানে α দেখুন। একটিতেও α মিথ্যা হলে উত্তর “না”। একে বলে model checking, আর পাঠ্যবইয়ে এর নাম TT-ENTAILS (truth table দিয়ে entailment). নিচের কোডে TELL আর ASK দুটিই আছে। ASK তিন রকম উত্তর দেয়: KB ⊨ α হলে “yes”, KB ⊨ ¬α হলে “no”, কোনোটিই না হলে “unknown”.

from itertools import product
SYMS = ["B", "F", "D", "S", "P"]
imp = lambda a, b: (not a) or b
# B: order above 1000 tk   F: free delivery   D: address inside Dhaka
# S: same-day delivery     P: pre-order item
kb = [lambda m: imp(m["B"], m["F"]),               # R1  B -> F
      lambda m: imp(m["F"] and m["D"], m["S"]),     # R2  F and D -> S
      lambda m: imp(m["P"], not m["S"])]            # R3  P -> not S
models = [dict(zip(SYMS, v)) for v in product([True, False], repeat=len(SYMS))]

def tell(sentence):
    kb.append(sentence)

def entails(alpha):                     # TT-ENTAILS by enumerating all models
    return all(alpha(m) for m in models if all(s(m) for s in kb))

def ask(alpha):
    if entails(alpha): return "yes"
    if entails(lambda m: not alpha(m)): return "no"
    return "unknown"

queries = {"S": lambda m: m["S"], "P": lambda m: m["P"],
           "F and not P": lambda m: m["F"] and not m["P"]}
print("models checked each time:", len(models), "= 2 **", len(SYMS))
for fact, f in [("B", lambda m: m["B"]), ("D", lambda m: m["D"])]:
    tell(f)
    kb_models = [m for m in models if all(s(m) for s in kb)]
    print(f"TELL {fact} -> models of KB: {len(kb_models)}")
    for name, q in queries.items():
        print(f"   ASK {name:12} {ask(q)}")
for m in kb_models:
    print("the only model left:", {k: int(v) for k, v in m.items()})

models checked each time: 32 = 2 ** 5
TELL B -> models of KB: 4
   ASK S            unknown
   ASK P            unknown
   ASK F and not P  unknown
TELL D -> models of KB: 1
   ASK S            yes
   ASK P            no
   ASK F and not P  yes
the only model left: {'B': 1, 'F': 1, 'D': 1, 'S': 1, 'P': 0}

2ⁿ-এর দেয়াল

Model checking sound আর complete (অংশ ৫-এ সংজ্ঞা): যা বলে তা ঠিক, আর যা entailed তা ধরে। সমস্যা খরচে। n-টি symbol-এ 2ⁿটি model:

দোকানের পুরো নিয়মের খাতায় একশো symbol খুব সাধারণ, আর চিপের নকশা যাচাইয়ে লাখ লাখ। এটা পর্ব ৪৩-এর সেই combinatorial explosion. দুটি পথে বেরোনো যায়: model না গুনে বাক্য থেকে বাক্যে যুক্তি চালানো (অংশ ৫–৭), অথবা চালাকি করে model খোঁজা (অংশ ৮)।

৫ · Inference rule — modus ponens থেকে sound আর complete

মানুষ যুক্তি দেন truth table না বানিয়ে: “অর্ডার বড়; বড় হলে ফ্রি; তাই ফ্রি”। এই ধরনের এক ধাপের ছাঁচকে বলে inference rule. লেখা হয় দাগের ওপরে যা জানা (premise), নিচে যা বের হলো। নতুন বাক্য বের করাকে বলে derive, চিহ্ন ⊢ (KB ⊢ α মানে “KB থেকে নিয়ম খাটিয়ে α পাওয়া যায়”)।

বাজারঘরের প্রশ্নে এক লাইন করে প্রমাণ: (১) B আর R1 থেকে modus ponens-এ F; (২) F আর D থেকে F ∧ D; (৩) F ∧ D আর R2 থেকে modus ponens-এ S; (৪) S আর R3 থেকে modus tollens-এ ¬P. চারটি ধাপ, অথচ model checking ৩২টি জগৎ ঘুরেছিল। প্রমাণ খোঁজা নিজেই একটি search সমস্যা: state = এ পর্যন্ত জানা বাক্যের সেট, action = একটি নিয়ম খাটানো, goal = α পাওয়া।

Sound আর complete — দুটি আলাদা প্রতিশ্রুতি

পরীক্ষার খাতা দেখার সঙ্গে তুলনা করুন: sound পরীক্ষক কখনো ভুল উত্তরে নম্বর দেন না; complete পরীক্ষক কোনো সঠিক উত্তর বাদ দেন না। আমরা দুটিই চাই, সঙ্গে দ্রুতও। পরের দুই অংশে একটিমাত্র নিয়ম, resolution, যা propositional logic-এ দুটি শর্তই মেটায়, যদি বাক্যগুলো একটি বিশেষ রূপে থাকে।

৬ · CNF — যেকোনো বাক্যকে clause-এর তালিকায়

কয়েকটি শব্দ আগে। Literal মানে একটি symbol বা তার negation: S, ¬S. Clause মানে কয়েকটি literal-এর ∨, যেমন ¬F ∨ ¬D ∨ S; সংক্ষেপে সেট হিসেবে লেখা হয় {¬F, ¬D, S}। একটি বাক্য CNF (conjunctive normal form) রূপে থাকে যদি তা কয়েকটি clause-এর ∧ হয়। “Clause-গুলোর প্রতিটি সত্য হতে হবে, আর প্রতিটি clause-এ অন্তত একটি literal সত্য হতে হবে।” প্রতিটি propositional বাক্যের একটি equivalent CNF আছে, আর তা বানানোর চারটি যান্ত্রিক ধাপ:

1. ↔ বাদ: α ↔ β ≡ (α → β) ∧ (β → α)
2. → বাদ: α → β ≡ ¬α ∨ β
3. ¬ ভেতরে ঢোকানো: De Morgan, ¬(α ∧ β) ≡ ¬α ∨ ¬β আর ¬(α ∨ β) ≡ ¬α ∧ ¬β; সঙ্গে ¬¬α ≡ α
4. ∨-কে ∧-এর ওপর ছড়ানো (distribution): α ∨ (β ∧ γ) ≡ (α ∨ β) ∧ (α ∨ γ)

ধরুন বাজারঘর R2-কে আরও কড়া করল: “একই দিনে delivery হয় ঠিক তখনই, যখন delivery ফ্রি আর ঠিকানা ঢাকায়”, মানে S ↔ (F ∧ D). নিচের stepper এটিকে CNF-এ আনে।

1a<->b => (a->b)&(b->a)2a->b => ~a|b3~(a&b) => ~a|~b4a|(b&c) => (a|b)&(a|c)

অংশ ৮-এর sympy run-এ to_cnf একই তিনটি clause দিয়েছে, শুধু ক্রম আলাদা। সতর্কতা: distribution খারাপ ক্ষেত্রে বাক্যকে বিস্ফোরিত করে। (A₁ ∧ B₁) ∨ (A₂ ∧ B₂) ∨ … ∨ (A_n ∧ B_n)-এর সরাসরি CNF-এ 2ⁿটি clause. বাস্তবের solver তাই Tseitin transformation ব্যবহার করে: প্রতিটি উপ-রাশির জন্য একটি নতুন symbol, ফলে আকার রৈখিক থাকে; নতুন বাক্যটি equivalent নয়, কিন্তু satisfiable হয় ঠিক তখনই, যখন মূলটি হয় (equisatisfiable).

৭ · Resolution refutation — ¬α যোগ করে খালি clause

Resolution নিয়মটি একটি লাইনে: একটি clause-এ L আর অন্যটিতে ¬L থাকলে, দুটি জুড়ে L আর ¬L বাদ দিয়ে নতুন clause. যেমন {¬B, F} আর {B} থেকে {F}; {¬F, ¬D, S} আর {¬S} থেকে {¬F, ¬D}। নতুনটির নাম resolvent. কেন sound: যেকোনো model-এ L সত্য হলে দ্বিতীয় clause-এর বাকি অংশ সত্য হতেই হবে, মিথ্যা হলে প্রথমটির বাকি অংশ; দুই ক্ষেত্রেই resolvent সত্য। Modus ponens আসলে এর একটি বিশেষ রূপ।

প্রমাণের কৌশলটি উল্টো দিক থেকে, যাকে বলে resolution refutation বা proof by contradiction: KB ⊨ α ঠিক তখনই, যখন KB ∧ ¬α unsatisfiable. তাই KB-র clause-এর সঙ্গে ¬α-এর clause যোগ করুন, আর resolve করতে থাকুন। যদি কোনো সময় empty clause {} পাওয়া যায় (যেমন {D} আর {¬D} থেকে), তার মানে স্ববিরোধ: KB আর ¬α একসঙ্গে সত্য হতে পারে না, তাই α প্রমাণিত।

এবার হাতে একটি পুরো প্রমাণ। প্রশ্ন: বাজারঘরের KB (R1, R2, R3, B, D) থেকে কি ¬P বেরোয়, মানে পণ্যটি pre-order নয়? CNF-এ KB-র পাঁচটি clause: C1 {¬B, F}, C2 {¬F, ¬D, S}, C3 {¬P, ¬S}, C4 {B}, C5 {D}। প্রমাণ করতে চাই ¬P, তাই তার উল্টো ¬¬P = P যোগ: C6 {P}।

1S = CNF(KB) + CNF(~goal)2pick L in Ci, ~L in Cj3add (Ci-L) | (Cj-~L)4empty? goal proved

হাতে আমরা জানতাম কোন জোড়া বাছতে হবে। যন্ত্র জানে না; তাকে জোড়া খুঁজতে হয়। নিচের কোড একটি সহজ কৌশল নেয়, যার নাম set of support: প্রতিটি resolution-এ অন্তত একটি clause আসবে ¬α থেকে বা তার বংশধর থেকে। এতে KB-র নিজেদের মধ্যের অপ্রাসঙ্গিক জোড়া বাদ যায়, আর resolution-এর refutation completeness-ও টিকে থাকে (Wos ও সহকর্মীরা ১৯৬৫)। Tautology resolvent (যেমন {S, ¬S}) ফেলে দেওয়া হয়, কারণ তা কখনো খালি clause-এর দিকে এগোয় না।

def neg(l):
    return l[1:] if l.startswith("~") else "~" + l

def resolvents(c1, c2):
    out = []
    for l in c1:
        if neg(l) in c2:
            r = (c1 - {l}) | (c2 - {neg(l)})
            if not any(neg(x) in r for x in r):     # drop tautologies
                out.append(frozenset(r))
    return out

def show(c):
    return "{" + ", ".join(sorted(c)) + "}" if c else "{} EMPTY"

def refute(kb, goal):        # set of support: start from the negated goal
    known = [frozenset(c) for c in kb]
    sos = [frozenset([neg(goal)])]
    print("goal:", goal, "| add", show(sos[0]))
    step = 0
    while sos:
        c = sos.pop(0)
        for d in list(known):
            for r in resolvents(c, d):
                if r in known or r in sos or r == c: continue
                step += 1
                print(f"  {step}. {show(c)} + {show(d)} -> {show(r)}")
                if not r: return "proved"
                sos.append(r)
        known.append(c)
    return "no empty clause: not entailed"

rules = [{"~B", "F"}, {"~F", "~D", "S"}, {"~P", "~S"}]  # R1 R2 R3 in CNF
print(refute(rules + [{"B"}, {"D"}], "~P"))
print(refute(rules + [{"B"}], "S"))                     # D is not known

goal: ~P | add {P}
  1. {P} + {~P, ~S} -> {~S}
  2. {~S} + {S, ~D, ~F} -> {~D, ~F}
  3. {~D, ~F} + {F, ~B} -> {~B, ~D}
  4. {~D, ~F} + {D} -> {~F}
  5. {~B, ~D} + {B} -> {~D}
  6. {~B, ~D} + {D} -> {~B}
  7. {~D} + {D} -> {} EMPTY
proved
goal: S | add {~S}
  1. {~S} + {S, ~D, ~F} -> {~D, ~F}
  2. {~D, ~F} + {F, ~B} -> {~B, ~D}
  3. {~B, ~D} + {B} -> {~D}
no empty clause: not entailed

৮ · Horn clause আর SAT — DPLL থেকে আধুনিক solver

Horn clause — বাস্তবের নিয়মের সস্তা রূপ

বাজারঘরের clause-গুলো দেখুন: {¬B, F}, {¬F, ¬D, S}, {¬P, ¬S}, {B}, {D}। প্রতিটিতে বড়জোর একটি positive (¬ ছাড়া) literal. এমন clause-কে বলে Horn clause (যুক্তিবিদ Alfred Horn-এর নামে, ১৯৫১)। ঠিক একটি positive literal থাকলে তা definite clause, আর সেটিকে “যদি … তাহলে” রূপে পড়া যায়: {¬F, ¬D, S} মানে (F ∧ D) → S. Positive literal একটিও না থাকলে ({¬P, ¬S}) তা একটি নিষেধ, (P ∧ S) → মিথ্যা।

Horn clause-এর সুবিধা বিশাল। সেখানে entailment-এর জন্য resolution-এর অন্ধ জোড়া-খোঁজার দরকার নেই: জানা তথ্য থেকে শুরু করে যে নিয়মের সব শর্ত পূরণ, তার ফল যোগ করতে থাকুন, যতক্ষণ নতুন কিছু আসে (forward chaining); অথবা প্রশ্ন থেকে পিছিয়ে শর্ত খুঁজুন (backward chaining). দুটিই KB-র আকারের সমানুপাতিক সময়ে চলতে পারে (Horn-SAT-এর linear-time অ্যালগরিদম, Dowling ও Gallier ১৯৮৪)। অংশ ৫-এর চার লাইনের প্রমাণটি আসলে forward chaining. ব্যবসার নিয়ম, expert system আর Prolog এই রূপের ওপর দাঁড়িয়ে; বিস্তারিত পর্ব ৪৭-এ (Rule-based আর expert system). সীমাটি হলো “অথবা”: “ঢাকা অথবা চট্টগ্রামে একই দিনে” ধরনের {S₁, S₂} clause Horn নয়।

SAT সমস্যা আর DPLL

একটি CNF বাক্য দেওয়া আছে; এমন model আছে কি, যা প্রতিটি clause সত্য করে? এই প্রশ্নের নাম SAT (Boolean satisfiability). Entailment আর SAT একই মুদ্রার দুই পিঠ: KB ⊨ α মানে KB ∧ ¬α-এর SAT উত্তর “না”। ১৯৭১ সালে Stephen Cook দেখান SAT NP-complete (Leonid Levin স্বাধীনভাবে কাছাকাছি সময়ে; তাই Cook–Levin theorem), মানে খারাপতম ক্ষেত্রে দ্রুত পদ্ধতি জানা নেই, আর পাওয়া গেলে তা P বনাম NP প্রশ্নের উত্তর দেবে।

তবু truth table-এর চেয়ে অনেক ভালো করা যায়। DPLL (Davis–Putnam ১৯৬০, Davis–Logemann–Loveland ১৯৬২) হলো CNF-এর ওপর পর্ব ৪৩-এর backtracking, তিনটি কৌশলসহ:

• Unit propagation: কোনো clause-এ একটিই literal বাকি থাকলে তার মান বাধ্যতামূলক। CSP-র MRV আর forward checking-এর মতো। Horn KB-তে শুধু এটিই forward chaining.
• Pure literal: কোনো symbol সব জায়গায় একই চিহ্নে এলে (শুধু E, কোথাও ¬E নয়) তাকে সেই মান দিলে কোনো ক্ষতি নেই।
• Splitting: আর কিছু না চললে একটি symbol বেছে আগে T, ব্যর্থ হলে F দিয়ে চেষ্টা; এখানেই backtracking.

নিচের stepper ছয়টি clause-এর একটি ছোট বাক্যে DPLL চালায়: 1 {A, B}, 2 {¬A, C}, 3 {¬B, C}, 4 {¬C, D}, 5 {¬A, ¬D}, 6 {E, B}। “✓” মানে clause সত্য হয়ে গেছে, তালিকা থেকে বাদ।

1while unit: assign it2pure literal: assign3empty clause: undo4else split: T, then F5none left: SAT

এই তিনটি কৌশল ডেস্কটপে Python-এ লিখে (প্রায় ৪০ লাইন, শুধু standard library) seed 42-এর এলোমেলো 3-SAT-এ চালানো হলো: প্রতিটি clause-এ তিনটি literal, clause-এর সংখ্যা variable-এর প্রায় ৪.২৬ গুণ। পাশে truth table, যা প্রথম সত্য সারি পেলেই থামে। সত্যিকারের run (Python 3.14.4, একটি ল্যাপটপ, একটি run):

~/bazarghar-logic$ python dpll_run.py
Python 3.14.4
n= 10 m= 43 DPLL sat=False splits=    4 units=    20 pures=   0 time=0.000s | truth table: 1,024 of 2^10=1,024 rows, 0.00s
n= 16 m= 68 DPLL sat=True  splits=    5 units=    10 pures=   0 time=0.000s | truth table: 23,135 of 2^16=65,536 rows, 0.04s
n= 20 m= 85 DPLL sat=True  splits=   11 units=    90 pures=   1 time=0.001s | truth table: 170,168 of 2^20=1,048,576 rows, 0.27s
n= 50 m=213 DPLL sat=False splits=  202 units=  2459 pures=  39 time=0.059s
n=100 m=426 DPLL sat=True  splits= 5521 units=106594 pures=1479 time=5.499s

২০টি variable-এ truth table ১,৭০,১৬৮টি সারি দেখেছে, DPLL মাত্র ১১টি split. ৫০ আর ১০০ variable-এ truth table চালানোই হয়নি (2¹⁰⁰). কিন্তু খেয়াল করুন, DPLL-এর split-ও দ্রুত বাড়ছে: ৫০-এ ২০২, ১০০-তে ৫,৫২১ আর সাড়ে পাঁচ সেকেন্ড। এখানেই আধুনিক solver আলাদা।

আধুনিক SAT solver — সত্যিকারের run

১৯৯০-এর দশকের শেষ থেকে CDCL (conflict-driven clause learning) পদ্ধতি এসেছে: প্রতিটি সংঘাতের কারণ বিশ্লেষণ করে একটি নতুন clause “শেখা” হয়, যাতে একই ভুল আর না হয়; সঙ্গে অনেক দূর এক লাফে পিছোনো, নিয়মিত restart আর চতুর variable-বাছাই। GRASP (Marques-Silva ও Sakallah), Chaff (২০০১) আর MiniSat (Eén ও Sörensson) এই ধারার পরিচিত নাম; CaDiCaL আর Kissat (Armin Biere ও সহকর্মীরা) সাম্প্রতিক বছরগুলোর SAT Competition-এ ভালো করেছে বলে প্রকাশিত ফলাফলে দেখা যায়। চিপের নকশা যাচাই, software verification আর কিছু package manager-এর dependency সমাধানে SAT-ভিত্তিক পদ্ধতির ব্যবহার প্রকাশিত, তবে কোন প্রতিষ্ঠান ঠিক কোনটি চালায় তা সাধারণত প্রকাশ্য নয়।

Python থেকে এগুলো ব্যবহারের দুটি পরিচিত প্যাকেজ: pycosat (PicoSAT solver-এর binding) আর python-sat (PySAT, import করার নাম pysat, যাতে MiniSat, Glucose, CaDiCaL-সহ অনেক solver). দুটিই C-তে লেখা extension, ব্রাউজারের Python-এ নেই, তাই ডেস্কটপে চালানো হলো। লেখার সময়ে PyPI-তে সর্বশেষ pycosat 0.6.6 আর python-sat 1.9.dev20; শেষেরটির প্রায় সব release-ই এমন .devN নামে প্রকাশিত হয়, আর এই প্যাকেজে pip install python-sat সেটিই বসিয়েছে। Clause লেখা হয় DIMACS ধাঁচে: প্রতিটি symbol একটি সংখ্যা, ঋণাত্মক মানে ¬. মূল অংশটুকু:

import random, time
import pycosat
from pysat.solvers import Solver
from pysat.examples.genhard import PHP

kb = [[-1, 2], [-2, -3, 4], [-5, -4], [1], [3]]    # B=1 F=2 D=3 S=4 P=5
print("pycosat model:", pycosat.solve(kb))
print("number of models:", sum(1 for _ in pycosat.itersolve(kb)))
print("KB + [-S]:", pycosat.solve(kb + [[-4]]), "-> KB entails S")

def rand3sat(n, m, seed):
    rng = random.Random(seed)
    return [[v * rng.choice((1, -1)) for v in rng.sample(range(1, n + 1), 3)]
            for _ in range(m)]

def run(name, clauses):
    with Solver(name=name, bootstrap_with=clauses) as s:
        t = time.perf_counter()
        ok = s.solve()
        dt = time.perf_counter() - t
        st = s.accum_stats()
    return ok, dt, st.get("decisions"), st.get("conflicts")

for n, ratio in [(1000, 3.0), (200, 4.26), (300, 4.26), (400, 4.26)]:
    cl = rand3sat(n, int(n * ratio), 42)
    for name in ("minisat22", "cadical195"):
        ok, dt, dec, con = run(name, cl)          # printed as aligned columns
for holes in (6, 7, 8, 9, 10):                     # n+1 pigeons, n holes
    cnf = PHP(holes)
    ok, dt, dec, con = run("cadical195", cnf.clauses)

ওপরে শুধু মূল অংশ; পুরো স্ক্রিপ্টে এর বাইরে আছে version আর সারিবদ্ধ করে ছাপানোর কয়েকটি print লাইন। সত্যিকারের run (Python 3.14.4, pycosat 0.6.6, python-sat 1.9.dev20, একটি ল্যাপটপ, একটি run):

~/bazarghar-logic$ python sat_run.py
Python 3.14.4 | pycosat 0.6.6 | python-sat 1.9.dev20

[1] bazarghar KB
pycosat model: [1, 2, 3, 4, -5]
number of models: 1
KB + [-S]: UNSAT -> KB entails S

[2] random 3-SAT (seed 42)
n= 1000 m= 3000 minisat22  sat=True  time=  0.001s decisions=     393 conflicts=      50
n= 1000 m= 3000 cadical195 sat=True  time=  0.002s decisions=     541 conflicts=      73
n=  200 m=  852 minisat22  sat=True  time=  0.011s decisions=    3244 conflicts=    2623
n=  200 m=  852 cadical195 sat=True  time=  0.016s decisions=    2181 conflicts=    1905
n=  300 m= 1278 minisat22  sat=False time= 40.066s decisions= 6277311 conflicts= 5237004
n=  300 m= 1278 cadical195 sat=False time=102.410s decisions= 2925159 conflicts= 1808152
n=  400 m= 1704 minisat22  sat=True  time= 35.026s decisions= 4698318 conflicts= 3811812
n=  400 m= 1704 cadical195 sat=True  time=  2.637s decisions=  233828 conflicts=  120032

[3] pigeonhole PHP
 7 pigeons  6 holes vars= 42 clauses= 133 sat=False time=  0.003s conflicts=    1044
 8 pigeons  7 holes vars= 56 clauses= 204 sat=False time=  0.030s conflicts=    7130
 9 pigeons  8 holes vars= 72 clauses= 297 sat=False time=  0.197s conflicts=   31719
10 pigeons  9 holes vars= 90 clauses= 415 sat=False time=  2.517s conflicts=  267023
11 pigeons 10 holes vars=110 clauses= 561 sat=False time= 25.756s conflicts= 2227032

• বাজারঘর: model [1, 2, 3, 4, -5] মানে B, F, D, S সত্য, P মিথ্যা, ঠিক অংশ ৪-এর একমাত্র model. KB-তে ¬S যোগ করলে UNSAT, মানে KB ⊨ S.
• আকার নয়, গঠন কঠিন করে: ১,০০০ variable, অনুপাত ৩.০: হাজার ভাগের এক সেকেন্ড। ৩০০ variable, অনুপাত ৪.২৬: ৪০ সেকেন্ড (MiniSat) আর ১০২ সেকেন্ড (CaDiCaL), উত্তর UNSAT. এলোমেলো 3-SAT-এ অনুপাত প্রায় ৪.২-এর কাছে সমস্যা সবচেয়ে কঠিন হয়, যাকে phase transition বলে (Mitchell, Selman আর Levesque ১৯৯২-এর পরীক্ষা থেকে পরিচিত)।
• কোন solver ভালো, তা সমস্যায় নির্ভর করে: ৩০০-তে MiniSat দ্রুত, ৪০০-তে CaDiCaL ১৩ গুণ দ্রুত। এক run, এক যন্ত্র, এক seed; সাধারণ নিয়ম নয়।
• Pigeonhole: “n+1টি পায়রা n-টি খোপে, প্রতি খোপে একটি” সবসময় অসম্ভব, মানুষ এক লাইনে বোঝেন। অথচ প্রতি খোপ বাড়ালে সময় প্রায় দশ গুণ: ১১টি পায়রায় ২৬ সেকেন্ড। ১৯৮৫ সালে Armin Haken প্রমাণ করেন, resolution দিয়ে এর প্রতিটি প্রমাণ exponential আকারের; CDCL-এর প্রমাণও resolution-এর একটি রূপ, তাই এই দেয়াল তারও।

ব্রাউজারেও একটি পরীক্ষা চালানো যায়: Pyodide-এ sympy প্যাকেজ আছে, যার sympy.logic CNF বানায়, satisfiable খোঁজে আর বাক্য সরল করে। এর SAT অংশ Python-এ লেখা DPLL-ধাঁচের, বড় সমস্যার জন্য নয়, কিন্তু হাতের কাজ যাচাইয়ে চমৎকার। প্রথমবার sympy নামতে কয়েক সেকেন্ড লাগতে পারে।

import sympy
from sympy import symbols
from sympy.logic.boolalg import Implies, Equivalent, to_cnf, simplify_logic
from sympy.logic.inference import satisfiable

B, F, D, S, P = symbols("B F D S P")
print("sympy", sympy.__version__)
print("CNF of S <-> (F & D):", to_cnf(Equivalent(S, F & D)))

kb = Implies(B, F) & Implies(F & D, S) & Implies(P, ~S) & B & D
m = satisfiable(kb)
print("a model of KB:", {str(k): int(v) for k, v in sorted(m.items(), key=str)})
print("KB & ~S satisfiable?", satisfiable(kb & ~S))   # False -> KB entails S
print("KB & P  satisfiable?", satisfiable(kb & P))    # False -> KB entails ~P

rules = Implies(B, F) & Implies(F & D, S) & Implies(P, ~S)
print("models of rules alone:", len(list(satisfiable(rules, all_models=True))))
print("simplified rules:", simplify_logic(rules, form="cnf"))
print("De Morgan valid?", not satisfiable(~Equivalent(~(B & F), ~B | ~F)))

sympy 1.14.0
CNF of S <-> (F & D): (D | ~S) & (F | ~S) & (S | ~D | ~F)
a model of KB: {'B': 1, 'D': 1, 'F': 1, 'P': 0, 'S': 1}
KB & ~S satisfiable? False
KB & P  satisfiable? False
models of rules alone: 14
simplified rules: (F | ~B) & (~P | ~S) & (S | ~D | ~F)
De Morgan valid? True

৯ · Propositional logic-এর সীমা — আর symbolic AI কোথায় দাঁড়ায়

বাজারঘরের পাঁচটি symbol একটি অর্ডারের কথা বলে। দোকানে দিনে হাজারো অর্ডার। “প্রতিটি অর্ডার ৳১,০০০-এর বেশি হলে তার delivery ফ্রি” লিখতে propositional logic-এ প্রতিটি অর্ডারের জন্য আলাদা symbol আর আলাদা নিয়ম লাগবে: B₁ → F₁, B₂ → F₂, … এই ভাষায় বস্তু (অর্ডার, কাস্টমার), তাদের সম্পর্ক (“এই কাস্টমারের অর্ডার”) আর “প্রতিটি” বা “অন্তত একটি” বলার উপায় নেই। এগুলো আনে first-order logic, যার ∀ (সব) আর ∃ (অন্তত একটি) চিহ্ন পর্ব ৪৬-এর (First-order logic — বস্তু, সম্পর্ক আর quantifier) বিষয়।

আরও তিনটি সীমা মাথায় রাখুন:

• অনিশ্চয়তা নেই: প্রতিটি কথা পুরো সত্য বা পুরো মিথ্যা। “ঢাকার ঠিকানায় সাধারণত ৯০% অর্ডার একই দিনে পৌঁছায়” লেখার জায়গা নেই। সম্ভাবনা দিয়ে যুক্তি মডিউল ৯-এ, পর্ব ৫০ (Bayes-এর উপপাদ্য) থেকে।
• Symbol-এর মানে বাইরে থেকে আসে: “D = ঠিকানা ঢাকায়” কে ঠিক করবেন? কাস্টমারের লেখা “Mirpur 10, Dhaka” থেকে D বের করা যুক্তির কাজ নয়, পড়া আর বোঝার কাজ, যেখানে machine learning প্রায়ই দরকার।
• জ্ঞান লেখার খরচ আর ভঙ্গুরতা: হাজারো নিয়ম হাতে লেখা, হালনাগাদ রাখা আর পরস্পরবিরোধী নিয়ম ধরা কঠিন; এর নাম knowledge acquisition bottleneck, আর নিয়মের বাইরের ঘটনায় হঠাৎ ভেঙে পড়াকে বলে brittleness.

তবু propositional logic আর SAT পুরোনো জিনিস নয়, machine learning-এর প্রতিদ্বন্দ্বীও নয়। এর শক্তি যেখানে: নিশ্চয়তা (UNSAT মানে প্রমাণসহ “অসম্ভব”), ব্যাখ্যা (প্রতিটি সিদ্ধান্তের পেছনে কোন নিয়ম, তা দেখানো যায়; explainability), আর ডেটা ছাড়া কাজ (নতুন নিয়ম এলেই চলে, হাজারো উদাহরণ লাগে না)। তাই চিপ যাচাই, নিরাপত্তা-নীতির পরীক্ষা, সময়সূচি আর AI মডেলের চারপাশে নিয়মের পাহারা (guardrail) এখনো যুক্তির ভাষায় লেখা হয়। দুটি পথ মেলানোর গবেষণাকে বলে neuro-symbolic AI; কোন মিশ্রণ শেষ পর্যন্ত কাজের, তা নিয়ে গবেষকদের মতভেদ আছে।

১০ · AI-এর যুগে — AI সহকারী দিয়ে যুক্তি আর নিয়ম যাচাই

AI সহকারীকে “এই নিয়মগুলো থেকে কি X প্রমাণ হয়?” জিজ্ঞেস করলে সে সাবলীল ভাষায় একটি “প্রমাণ” লিখে দেবে। ভাষার মডেল (পর্ব ৭০-এ বিস্তারিত) পরের শব্দের সম্ভাব্য অনুমান থেকে লেখে; লম্বা যুক্তির শৃঙ্খলে একটি ভুল ধাপ সুন্দর বাক্যের আড়ালে লুকিয়ে থাকতে পারে। নিরাপদ ভাগাভাগি: AI সহকারী নিয়মকে symbol আর clause-এ লিখতে সাহায্য করুক, truth table বা solver যাচাই করুক, আর আপনি ছোট একটি ক্ষেত্রে হাতে মিলিয়ে নিন। এ ধরনের কাজে AI সহকারীরা প্রায়ই যা করে:

• Converse গুলিয়ে ফেলা: “B → F, তাই F → B” বা “ফ্রি পেয়েছেন, তাই অর্ডার বড়” ধরনের affirming the consequent, আত্মবিশ্বাসের সঙ্গে।
• → ভুল কোডে লেখা: a and b দিয়ে implication, বা satisfiable আর entailment গুলিয়ে any-এর জায়গায় all (বা উল্টো)।
• বানানো বা পুরোনো API: sympy-তে অস্তিত্বহীন function, pysat-এ ভুল solver-নাম, বা pycosat আর python-sat-এর clause-ধাঁচ মিশিয়ে ফেলা।
• স্ববিরোধী KB না ধরা: KB নিজেই unsatisfiable হলে সব কথাই “entailed” হয়ে যায়; প্রথমে KB satisfiable কি না, তা না দেখে উত্তর দেওয়া।
• “প্রমাণিত” বলে যাচাইহীন দাবি: solver-এর status না দেখে, বা সময় ফুরিয়ে যাওয়া run-কে UNSAT ধরে নেওয়া।

AI-এর লেখা যুক্তি বা logic-কোড হাতে পেলে — যাচাইয়ের চেকলিস্ট

• প্রতিটি symbol-এর মানে লিখে রেখেছি, আর প্রতিটি নিয়ম symbol-এ ঠিক দিকে (→-এর premise আর conclusion) বসেছে কি না দেখেছি
• প্রমাণের প্রতিটি ধাপ একটি নাম-জানা sound নিয়ম (modus ponens, resolution) কি না মিলিয়েছি; converse-এর লুকানো ব্যবহার খুঁজেছি
• ছোট উদাহরণে truth table বা model checking চালিয়ে AI-এর উত্তর স্বাধীনভাবে মিলিয়েছি
• KB নিজে satisfiable কি না আগে দেখেছি, যাতে স্ববিরোধী নিয়ম থেকে “সব প্রমাণিত” না হয়
• Solver-এর status (SAT, UNSAT, timeout) দেখে তবেই ফল পড়েছি; package আর function-এর নাম নিজের version-এর docs-এ খুঁজে পেয়েছি
• আসল কাস্টমার বা কর্মীর ব্যক্তিগত তথ্য প্রম্পটে দিইনি; উদাহরণের জন্য বানানো symbol আর ডেটা ব্যবহার করেছি