SAT আর SMT solver — discrete math দিয়ে software যাচাই

১ · SAT আবার — একটি প্রশ্নে হাজারো সমস্যা

পর্ব ০২ “Propositional logic”-এ proposition আর truth table, পর্ব ০৩ “Logical equivalence”-এ CNF আর satisfiability, আর পর্ব ০৭ “কাজে যুক্তি”-এ DPLL, Sudoku-র encoding আর Z3-এর প্রথম ব্যবহার দেখেছেন। মনে করিয়ে দিই: একটি clause কয়েকটি literal-এর ∨, আর CNF সূত্র কয়েকটি clause-এর ∧. সূত্রটি satisfiable, যদি এমন একটি মান-বসানো (model) থাকে যাতে প্রতিটি clause-এ অন্তত একটি literal সত্য।

এই অসমতাই SAT-কে বিশেষ করে। প্রস্তাবিত model দিলে প্রতিটি clause একবার দেখে polynomial সময়ে যাচাই করা যায়, তাই SAT NP শ্রেণিতে। আর Cook (১৯৭১) আর স্বাধীনভাবে Levin-এর উপপাদ্য বলে, NP-এর প্রতিটি সমস্যা polynomial সময়ে SAT-এ রূপান্তর করা যায় (Cook–Levin theorem; বক্তব্য পর্ব ০৭-এ, প্রমাণ এখানে বাদ)। তাই SAT NP-complete. Turing machine দিয়ে NP-এর নির্ভুল সংজ্ঞা আসছে পর্ব ৭৫ “Turing machine-এর পরিচয় — computability আর halting problem”-এ; reduction-এর পূর্ণ আলোচনা DSA কোর্সের পর্ব ৬৪-এ। গণনার মডেলের পূর্ণ তত্ত্ব পরিকল্পিত Theory of Computation কোর্সের বিষয়; এখানে আমরা discrete math-এর দিক থেকে দেখি: encoding-এর প্রমাণ, গণনা আর graph.

এই পর্বের পথ: প্রথমে solver কীভাবে খোঁজে (§২, §৪), তারপর সমস্যাকে কীভাবে সূত্রে লিখতে হয় (§৩), কোন ধরন সহজ (§৫), আর শেষে সংখ্যা ও bit-এর জগতে SMT দিয়ে কোড যাচাই (§৬–§৮)।

২ · DPLL-এ pure literal আর একটি পূর্ণ trace

পর্ব ০৭-এ DPLL-এর দুটি নিয়ম প্রমাণসহ দেখেছেন: unit propagation (একটি literal-এর clause থাকলে তার মান বাধ্য) আর শাখা করে backtracking. সেখানে তৃতীয় নিয়মটি বাদ ছিল। F|ℓ মানে ℓ সত্য ধরে সূত্র ছোট করা: ℓ-ওয়ালা clause বাদ, অন্য clause থেকে ¬ℓ মুছে ফেলা।

1. (⇒) F-এর একটি model M নিন, আর ℓ-এর variable-এর মান বদলে ℓ সত্য করুন; নাম দিন M′. — নির্মাণ
2. যে clause-এ ℓ আছে, M′-এ তা সত্য। যে clause-এ ℓ নেই, তাতে ¬ℓ-ও নেই (ℓ pure), অর্থাৎ ওই variable-ই নেই; তাই তার মান M-এর মতোই সত্য। M′ F-এর model, আর F|ℓ-এর clause-গুলো F-এর clause-এরই অংশ যেগুলো M′-এ সত্য। — ক্ষেত্র ভাগ
3. (⇐) F|ℓ-এর model-এ ℓ = সত্য যোগ করলে ℓ-ওয়ালা clause সত্য হয়, আর বাকি clause F|ℓ-এ অপরিবর্তিত ছিল (মোছার মতো ¬ℓ ছিল না)। ∎ — সংজ্ঞা

সাবধান: unit নিয়ম কোনো model হারায় না, কিন্তু pure নিয়ম হারাতে পারে (যে model-এ ℓ মিথ্যা, সেগুলো)। এটি শুধু satisfiability রাখে; দুটি সূত্রের এমন সম্পর্ককে equisatisfiable বলে। “সব model গোনা” কাজে pure নিয়ম চলবে না।

এবার তিনটি নিয়ম একসঙ্গে, পর্ব ০৭-এর চেয়ে আলাদা একটি সূত্রে। ক্রম: আগে unit, না থাকলে pure (সবচেয়ে ছোট variable), না থাকলে প্রথম clause-এর প্রথম variable-এ অনুমান।

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

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

DPLL-এর সঠিকতার প্রমাণ পর্ব ০৭-এর উপপাদ্য ৪.২ (খোলা variable-এর সংখ্যার ওপর strong induction); Lemma ২.১ সেই প্রমাণে আরেকটি ক্ষেত্র যোগ করে মাত্র, কারণ pure ধাপেও একটি variable কমে আর satisfiability বদলায় না। নিচের ব্লক এই DPLL লেখে, stepper-এর সূত্র মেলায়, তারপর n = 10 variable-এর এলোমেলো 3-CNF-এ উত্তরটি brute force-এর সঙ্গে মেলায়। Brute force-এ 2¹⁰ = 1024টি সারি একসঙ্গে একটি বড় পূর্ণসংখ্যার bit হিসেবে রাখা হয়েছে: variable v-এর “column” হলো যেসব সারিতে v সত্য তাদের bitmask, আর clause মানে mask-এর OR, সূত্র মানে AND. প্রথমবার চালালে ব্রাউজারে Python (Pyodide) নামতে কয়েক সেকেন্ড লাগে।

import random
def simplify(cnf, lit):                  # lit is now true
    return [[l for l in c if l != -lit] for c in cnf if lit not in c]
def dpll(cnf, trail, stats):
    while True:
        if [] in cnf: return None        # empty clause: conflict
        lits = {l for c in cnf for l in c}
        unit = next((c[0] for c in cnf if len(c) == 1), None)
        pure = min((l for l in lits if -l not in lits), key=abs, default=None)
        lit = unit if unit is not None else pure
        if lit is None: break
        trail, cnf = trail + [lit], simplify(cnf, lit)
    if not cnf: return trail             # every clause satisfied
    stats[0] += 1; x = abs(cnf[0][0])    # one decision (branch) on x
    return (dpll(simplify(cnf, x), trail + [x], stats)
            or dpll(simplify(cnf, -x), trail + [-x], stats))
def brute(cnf, n):                       # all 2^n rows at once, as bit masks
    N = 1 << n; full = rows = (1 << N) - 1   # bit a of rows: row a still OK
    col = [sum(1 << a for a in range(N) if a >> v & 1) for v in range(n)]
    for c in cnf:
        cm = 0
        for l in c: cm |= col[l - 1] if l > 0 else full ^ col[-l - 1]
        rows &= cm
    return rows != 0
print("stepper formula:", dpll([[1, -2], [-1, -3], [-1, 4], [-1, -4], [-4, 3, 2]], [], [0]))
random.seed(77); n, T = 10, 40
print(" m/n  SAT share  DPLL = brute  avg decisions")
for ratio in (2, 3, 4, 4.3, 5, 6):
    sat = agree = dec = 0
    for _ in range(T):
        F = [[v * random.choice((1, -1)) for v in random.sample(range(1, n + 1), 3)]
             for _ in range(round(ratio * n))]
        st = [0]; r = dpll(F, [], st) is not None
        sat += r; agree += r == brute(F, n); dec += st[0]
    print(f"{ratio:4}  {sat / T:9.2f}  {agree:7}/{T}  {dec / T:13.1f}")

stepper formula: [-1, -2, 3]
 m/n  SAT share  DPLL = brute  avg decisions
   2       1.00       40/40            2.2
   3       1.00       40/40            3.8
   4       0.80       40/40            4.5
 4.3       0.82       40/40            4.5
   5       0.42       40/40            5.1
   6       0.20       40/40            4.8

৩ · সমস্যাকে CNF-এ লেখা — graph coloring আর শিফট

Solver শুধু clause বোঝে; অর্থ থাকে encoding-এ। পর্ব ০৭-এ Sudoku-র “ঠিক একটি” নিয়ম দেখেছেন। এখানে পর্ব ৬৩-এর graph coloring: বাজারঘরের ডেলিভারি-এলাকাগুলোকে k-টি দিনে ভাগ করতে হবে, আর যে দুটি এলাকা একই রাস্তা ভাগ করে (graph-এ edge), তারা একই দিনে নয়। Sudoku নিজেও একটি নির্দিষ্ট graph-এর 9-coloring, যা পর্ব ৬৩-এ দেখেছেন।

1. (⇒) Proper coloring f: V → {1, …, k} দিলে x_v,c = T ঠিক তখন, যখন f(v) = c. প্রতিটি v-এ ঠিক একটি x_v,c সত্য, তাই (ক) আর (খ) সত্য। Edge uw-তে f(u) ≠ f(w), তাই কোনো c-তে x_u,c আর x_w,c দুটোই সত্য নয়: (গ) সত্য। — নির্মাণ
2. (⇐) একটি model নিন। (ক) বলে প্রতিটি v-এ অন্তত একটি রং, (খ) বলে বড়জোর একটি (পর্ব ০৭-এর উপপাদ্য ৩.১), তাই f(v) = সেই একমাত্র c একটি ফাংশন। (গ) বলে edge-এর দুই প্রান্তে একই c সত্য নয়, তাই f proper. — “ঠিক একটি”
3. দুই দিকের রূপান্তর একে অপরের উল্টো, তাই bijection: model-এর সংখ্যা = proper k-coloring-এর সংখ্যা। ∎ — পর্ব ১৬-এর inverse

ধাপ ৩ দেখায় কেন (খ) রাখা হয়েছে: শুধু “সম্ভব কি না” জানতে (খ) বাদ দিলেও চলে (একাধিক রং পেলে যেকোনো একটি নিলেই হয়), কিন্তু তখন model-এর সংখ্যা আর coloring-এর সংখ্যা সমান থাকে না। নিচে সবচেয়ে ছোট উদাহরণ, ত্রিভুজ K₃.

1vars: u1 u2 u3 v1 … w32u1 ∨ u2 ∨ u3  (×3)3¬u1 ∨ ¬u2 …  (×9)4¬u1 ∨ ¬v1 …  (×9)5model: u1 v2 w36k = 2: 12, UNSAT

নিচের ব্লক এই encoder লেখে আর আগের ব্লকের dpll দিয়ে সমাধান করে (দুই ব্লক একই namespace ভাগ করে, তাই আগেরটি আগে চলে)। পরীক্ষার graph: ত্রিভুজ, বাজারঘরের সাতটি এলাকা A–G, আর wheel W₅ (একটি কেন্দ্র H যুক্ত পাঁচ-cycle P, Q, R, S, T-এর সব vertex-এর সঙ্গে)। Model থেকে রং পড়ে আলাদা করে মেলানো হয় যে coloring সত্যিই proper.

from itertools import combinations
def colour_cnf(V, E, k):                 # variable x(v,c): "vertex v gets colour c"
    var = {}
    for v in V:
        for c in range(k):
            var[v, c] = len(var) + 1
    cnf = [[var[v, c] for c in range(k)] for v in V]                  # at least one
    cnf += [[-var[v, c], -var[v, d]] for v in V
            for c, d in combinations(range(k), 2)]                     # at most one
    cnf += [[-var[u, c], -var[w, c]] for u, w in E for c in range(k)]  # ends differ
    return var, cnf
def solve(name, V, E, k):
    var, cnf = colour_cnf(V, E, k)
    model = dpll(cnf, [], [0])
    head = f"{name}, k={k}: {len(var)} vars, {len(cnf)} clauses ->"
    if model is None:
        print(head, "UNSAT"); return
    col = {v: c for (v, c), i in var.items() if i in model}
    print(head, "".join(str(col[v]) for v in V),
          "proper:", all(col[u] != col[w] for u, w in E))
K3 = ["abc", ["ab", "bc", "ca"]]
solve("triangle", *K3, 2)
solve("triangle", *K3, 3)
zones = ["ABCDEFG", ["AB", "AC", "BC", "BD", "CD", "CE", "DF", "EF", "EG", "FG"]]
solve("zones", *zones, 3)
W5 = ["HPQRST", ["HP", "HQ", "HR", "HS", "HT", "PQ", "QR", "RS", "ST", "TP"]]
solve("wheel W5", *W5, 3)
solve("wheel W5", *W5, 4)
n, m = len(zones[0]), len(zones[1])
print("formula n + n*C(k,2) + m*k for zones, k=3:", n + n * 3 + m * 3)

triangle, k=2: 6 vars, 12 clauses -> UNSAT
triangle, k=3: 9 vars, 21 clauses -> 012 proper: True
zones, k=3: 21 vars, 58 clauses -> 0120012 proper: True
wheel W5, k=3: 18 vars, 54 clauses -> UNSAT
wheel W5, k=4: 24 vars, 82 clauses -> 012123 proper: True
formula n + n*C(k,2) + m*k for zones, k=3: 58

শিফটের শর্ত — দুই literal-এর clause

বাজারঘরের তিন রাইডার a, b, c. প্রত্যেকের একটি সত্য-মিথ্যা variable: সত্য মানে সকালের শিফট, মিথ্যা মানে বিকেলের। ম্যানেজারের শর্তগুলো প্রায়ই দুটি রাইডার নিয়ে: “a বা b অন্তত একজন সকালে” = (a ∨ b); “a সকালে হলে b-ও সকালে (একই ভ্যান)” = (¬a ∨ b); “b আর c একসঙ্গে সকালে নয় (একটিই বাইক)” = (¬b ∨ ¬c). প্রতিটি clause-এ বড়জোর দুটি literal: এটি 2-SAT, যা §৫-এ polynomial সময়ে মেলানো যাবে। কিন্তু “তিনজনের অন্তত একজন” লিখলে তিন literal-এর clause আসে, আর সমস্যা আবার সাধারণ SAT-এর মতো কঠিন হতে পারে।

৪ · CDCL আর কঠিন সূত্র — শেখা clause, pigeonhole আর phase transition

পর্ব ০৭-এ দেখেছেন, আধুনিক solver CDCL: বিরোধ হলে কারণ খুঁজে একটি নতুন clause শেখে। §২-এর stepper-এ বিরোধ ঘটিয়েছিল C3 = (¬a ∨ d) আর C4 = (¬a ∨ ¬d). পর্ব ০৬ “অনুমানের নিয়ম”-এর resolution নিয়মে d বাদ দিলে পাওয়া যায় (¬a): শেখা clause. বাস্তব solver-এ বিরোধের পেছনে কয়েক ডজন অনুমান থাকতে পারে, তবু শেখা clause-এ সাধারণত অল্প কয়েকটি literal থাকে।

প্রমাণ: F ∧ L-এর প্রতিটি model F-এরও model. উল্টো দিকে, resolution sound (পর্ব ০৬): দুটি clause (x ∨ A) আর (¬x ∨ B) সত্য হলে x যা-ই হোক A ∨ B সত্য। তাই F-এর প্রতিটি model-এ resolution-এর প্রতিটি ধাপের ফল, আর শেষে L, সত্য। ∎ তাই solver যত খুশি clause শিখতে পারে, উত্তর বদলায় না; শুধু একই ভুল দ্বিতীয়বার হয় না।

এর একটি গভীর পরিণাম আছে। কোনো সূত্রে CDCL “UNSAT” বললে তার শেখা clause-এর ইতিহাস আসলে একটি resolution প্রমাণ, যার শেষে empty clause. তাই resolution-এর জন্য যে সূত্র কঠিন, CDCL-এর জন্যও তা কঠিন। বিখ্যাত উদাহরণ পর্ব ৩২-এর pigeonhole নীতি: n + 1টি অর্ডার, n-টি স্লট, কোনো স্লটে দুটি অর্ডার নয়। Pigeonhole সূত্র PHPⁿ⁺¹_n-এ variable p_i,j = “অর্ডার i স্লট j-তে”: প্রতিটি অর্ডারের জন্য p_i,1 ∨ ⋯ ∨ p_i,n, আর প্রতিটি স্লট j ও অর্ডার-জোড়া i < i′-এর জন্য ¬p_i,j ∨ ¬p_i′,j. মোট n(n + 1)টি variable আর (n + 1) + n·C(n + 1, 2)টি clause. পর্ব ৩২ এক লাইনে প্রমাণ করেছে যে এটি UNSAT; কিন্তু Armin Haken ১৯৮৫ সালে প্রমাণ করেন, এর যেকোনো resolution প্রমাণের আকার n-এর exponential. মানুষের যুক্তি গোনে (“n + 1 > n”), resolution গুনতে পারে না।

সত্যিকারের run ১: pigeonhole সূত্রে Z3

নিচের পরীক্ষাগুলো এই কোর্সের লেখার সময় একটি সাধারণ Windows ডেস্কটপে সত্যিকারভাবে চালানো হয়েছে: Python 3.12, z3-solver 5.4.1 (Microsoft Research-এ তৈরি SMT solver, MIT লাইসেন্স), uv দিয়ে বানানো একটি ছোট প্রজেক্টে। নিজের কম্পিউটারে চালাতে চাইলে:

cd ~/bazarghar-dm
uv add z3-solver
uv run python php_sat.py

import time
from itertools import combinations
from z3 import Bool, Or, Not, SolverFor

# PHP(n+1, n): n+1 pigeons (orders), n holes (delivery slots), no sharing
def php(n):
    p = [[Bool(f"p{i}_{j}") for j in range(n)] for i in range(n + 1)]
    cls = [Or(row) for row in p]                                   # every pigeon gets a hole
    for j in range(n):
        cls += [Or(Not(p[a][j]), Not(p[b][j])) for a, b in combinations(range(n + 1), 2)]
    return cls

for n in range(6, 12):
    cls = php(n)
    s = SolverFor("QF_FD"); s.set("timeout", 60000)                # pure Boolean, 60 s cap
    s.add(cls)
    t0 = time.perf_counter(); r = s.check(); dt = time.perf_counter() - t0
    st = s.statistics()
    conf = st.get_key_value("sat conflicts") if "sat conflicts" in st.keys() else "?"
    print(f"n={n:2}: vars {n*(n+1):3}, clauses {len(cls):4}, {r}, {dt:7.2f} s, conflicts {conf}")

$ uv run python php_sat.py
n= 6: vars  42, clauses  133, unsat,    0.00 s, conflicts 605
n= 7: vars  56, clauses  204, unsat,    0.01 s, conflicts 1956
n= 8: vars  72, clauses  297, unsat,    0.09 s, conflicts 5832
n= 9: vars  90, clauses  415, unsat,    1.40 s, conflicts 37821
n=10: vars 110, clauses  561, unsat,    5.62 s, conflicts 110598
n=11: vars 132, clauses  738, unsat,   57.98 s, conflicts 958941

Clause-এর সংখ্যা সূত্র মেলায়: n = 6-এ 7 + 6 · 21 = 133. সূত্রের আকার মাত্র কয়েক শো clause, তবু বিরোধের সংখ্যা প্রতি ধাপে মোটামুটি ৩ থেকে ৯ গুণ বেড়েছে, আর n = 11-এ সময় প্রায় এক মিনিট (৬০ সেকেন্ডের সীমার একটু নিচে)। §৩-এর ৫৮ clause-এর সূত্র মুহূর্তে মিলেছিল; আকার নয়, গঠনই কঠিনতা ঠিক করে। কিছু solver এই কারণে গোনার যুক্তি (cardinality reasoning) বা symmetry ভাঙার কৌশল যোগ করে। সময়ের সংখ্যা যন্ত্রভেদে বদলাবে।

এলোমেলো 3-SAT-এর phase transition

§২-এর ব্লকে দেখেছেন, clause/variable অনুপাত বাড়লে satisfiable সূত্রের ভাগ হঠাৎ পড়ে যায়। বড় n-এ এই পতন প্রায় একটি ধাপের মতো তীক্ষ্ণ হয়, আর পরীক্ষা ও পরিসংখ্যান-পদার্থবিদ্যার হিসাবে এর অবস্থান অনুপাত প্রায় ৪.২৭; একে বলে phase transition বা দশা-বদল। সবচেয়ে কঠিন সূত্রগুলো ঠিক এই এলাকায়: কম অনুপাতে model প্রচুর, সহজে মেলে; বেশি অনুপাতে বিরোধ দ্রুত আসে। Friedgut ১৯৯৯ সালে দেখান যে তীক্ষ্ণ পতন ঘটে, আর বড় k-এর জন্য সঠিক সীমা পরে প্রমাণিত হয়েছে বলে জানা; k = 3-এর সঠিক মান এখনো প্রমাণিত নয় বলেই সাধারণভাবে উল্লেখ করা হয়। এখানে সংখ্যাটি একটি পর্যবেক্ষণ, উপপাদ্য নয়।

৫ · 2-SAT — implication graph আর SCC-তে polynomial সময়

দুই literal-এর clause (x ∨ y) আসলে দুটি শর্ত: x মিথ্যা হলে y সত্য, আর y মিথ্যা হলে x সত্য, অর্থাৎ ¬x → y আর ¬y → x. এই implication-গুলো দিয়ে একটি directed graph বানানো যায়।

দুটি সরল পর্যবেক্ষণ। (১) প্রতিটি edge একটি সত্য implication: F-এর যেকোনো model-এ ¬α সত্য হলে clause (α ∨ β)-এর জন্য β সত্য। Path-এ এটি শিকলের মতো চলে, তাই model-এ u সত্য আর u ⇝ v হলে v-ও সত্য (path-এর দৈর্ঘ্যের ওপর induction দিয়ে)। (২) Skew symmetry: u ⇝ v ⇔ ¬v ⇝ ¬u, কারণ edge জোড়ায় জোড়ায় আসে: ¬α → β-এর জোড়া ¬β → α, অর্থাৎ উল্টো দিকে নেগেশন (প্রমাণ অনুশীলন ১-এ)।

1. (⇐) ধরুন দুটি path-ই আছে, আর F-এর একটি model আছে। x সত্য হলে x ⇝ ¬x পর্যবেক্ষণ (১) অনুযায়ী ¬x-কে সত্য করে, বিরোধ। x মিথ্যা হলে ¬x সত্য, আর ¬x ⇝ x দিয়ে x সত্য, বিরোধ। তাই model নেই। — পর্যবেক্ষণ ১
2. (⇒) contrapositive: কোনো x-এ দুই path একসঙ্গে নেই ধরে একটি model বানাই। একটি মান-না-পাওয়া variable নিন; তার একটি literal ℓ বাছুন যাতে ℓ ⇝ ¬ℓ নেই (x ⇝ ¬x থাকলে ℓ = ¬x নিন; অনুমান অনুযায়ী তখন ¬x ⇝ x নেই)। ℓ থেকে পৌঁছানো যায় এমন সব literal সত্য করুন। — নির্মাণ
3. এতে বিরোধ নেই: ℓ ⇝ u আর ℓ ⇝ ¬u দুটোই হলে skew symmetry-তে u ⇝ ¬ℓ, তাই ℓ ⇝ u ⇝ ¬ℓ, যা ℓ বাছাইয়ের বিরোধী। আগের ধাপে মিথ্যা হওয়া কোনো u-তেও পৌঁছায় না: আগে বাছা ℓ′ ⇝ ¬u হলে skew symmetry-তে u ⇝ ¬ℓ′, তাই ℓ ⇝ ¬ℓ′, আবার skew symmetry-তে ℓ′ ⇝ ¬ℓ; তাহলে ¬ℓ আগেই সত্য হয়ে ℓ-এর variable মান পেয়ে যেত। — skew symmetry
4. প্রতিটি clause সত্য: (α ∨ β)-এ α মিথ্যা হলে ¬α সত্য, অর্থাৎ কোনো বাছা ℓ থেকে ¬α-তে পৌঁছানো যায়; edge ¬α → β থাকায় β-তেও, তাই β সত্য। সব variable মান না পাওয়া পর্যন্ত ধাপ ২–৩ চালালে একটি model পাওয়া যায়। ∎ — edge-এর সংজ্ঞা

SCC বের করা যায় O(n + m) সময়ে (Tarjan বা Kosaraju-র পদ্ধতি; graph-এর দিক পর্ব ৫৯-এ, আর C++/Python বাস্তবায়ন DSA কোর্সের পর্ব ৪৬-এ)। তাই 2-SAT রৈখিক সময়ে মেলে; এই রৈখিক-সময়ের পদ্ধতি সাধারণত Aspvall, Plass আর Tarjan-এর ১৯৭৯ সালের প্রবন্ধের নামে পরিচিত। “x ⇝ ¬x আছে কি” প্রশ্নটি আসলে পর্ব ৫৪-এর transitive closure-এর প্রশ্ন। §৩-এর তিন রাইডারের সঙ্গে চতুর্থ শর্ত যোগ করুন: “b সকালে হলে c-ও সকালে” = (¬b ∨ c).

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

C1a ∨ b   : ¬a→b, ¬b→aC2¬a ∨ b  : a→b, ¬b→¬aC3¬b ∨ c  : b→c, ¬c→¬bC4¬b ∨ ¬c : b→¬c, c→¬b

নিচের ব্লক উপপাদ্য ৫.২-এর প্রমাণটিকেই কোডে লেখে: প্রতিটি literal থেকে পৌঁছানো যায় এমন literal-এর সেট (ছোট n-এ এটুকুই যথেষ্ট; বড় n-এ SCC লাগে), x আর ¬x পরস্পর পৌঁছায় কি না পরীক্ষা, আর ধাপ ২–৩-এর নির্মাণে model. তারপর ৫১০টি এলোমেলো 2-CNF-এ brute force-এর সঙ্গে মেলায়, আর পাওয়া model সত্যিই সব clause মানে কি না দেখে।

import random
from itertools import product
def reach(G, s):                         # every literal reachable from s
    seen, todo = {s}, [s]
    while todo:
        for w in G[todo.pop()]:
            if w not in seen: seen.add(w); todo.append(w)
    return seen
def two_sat(clauses, n):
    G = {l: [] for v in range(1, n + 1) for l in (v, -v)}
    for a, b in clauses:                 # (a or b) gives -a -> b and -b -> a
        G[-a].append(b); G[-b].append(a)
    R = {l: reach(G, l) for l in G}
    if any(-v in R[v] and v in R[-v] for v in range(1, n + 1)):
        return None                      # v and -v in one SCC
    val = {}
    for v in range(1, n + 1):
        if v in val: continue
        l = -v if -v in R[v] else v      # never pick l with l ~> -l
        for u in R[l]: val[u], val[-u] = True, False
    return {v: val[v] for v in range(1, n + 1)}
def brute(clauses, n):
    return any(all(row[abs(a) - 1] == (a > 0) or row[abs(b) - 1] == (b > 0)
                   for a, b in clauses) for row in product((False, True), repeat=n))
print("stepper:", two_sat([(1, 2), (-1, 2), (-2, 3), (-2, -3)], 3))
print("drop last clause:", two_sat([(1, 2), (-1, 2), (-2, 3)], 3))
random.seed(7); n = 8; tests = agree = sat = 0
for m in range(4, 21):
    for _ in range(30):
        C = [tuple(v * random.choice((1, -1)) for v in random.sample(range(1, n + 1), 2))
             for _ in range(m)]
        val = two_sat(C, n); ok = val is not None
        good = not ok or all(val[abs(a)] == (a > 0) or val[abs(b)] == (b > 0) for a, b in C)
        tests += 1; sat += ok; agree += (ok == brute(C, n)) and good
print(f"{tests} random 2-CNFs (n=8, m=4..20): satisfiable {sat}, agree with brute force {agree}")

stepper: None
drop last clause: {1: True, 2: True, 3: True}
510 random 2-CNFs (n=8, m=4..20): satisfiable 395, agree with brute force 510

৬ · SMT — theory, DPLL(T) আর bit-vector

কোডের দাবিতে থাকে সংখ্যা: “i < n”, “x + y উপচে পড়ে না”. পর্ব ০৭-এ দেখেছেন, SMT solver এমন সূত্র সরাসরি নেয়। “Modulo theories” মানে প্রতিটি পরমাণু-শর্ত (atom) একটি নির্দিষ্ট theory-র ভেতরে ব্যাখ্যা করা হয়:

শেষ সারির কারণ Hilbert-এর দশম সমস্যা: Matiyasevich ১৯৭০ সালে (Davis, Putnam আর Robinson-এর আগের কাজের ওপর) প্রমাণ করেন, পূর্ণসংখ্যার polynomial সমীকরণের সমাধান আছে কি না, তা কোনো algorithm সব ক্ষেত্রে বলতে পারে না। তাই solver “unknown”-ও বলতে পারে।

DPLL(T) — SAT আর theory-র কথোপকথন

ধরুন F = (x < 3 ∨ y > 5) ∧ (x > 4) ∧ (y < 2), x, y পূর্ণসংখ্যা। প্রতিটি atom-এর জায়গায় একটি Boolean variable বসালে কাঠামো (p ∨ q) ∧ r ∧ s. SAT solver বলে: p, r, s সত্য। Theory solver পরীক্ষা করে x < 3 ∧ x > 4 ∧ y < 2, যা অসম্ভব, আর ফেরত দেয় শেখা clause (¬p ∨ ¬r). SAT solver এবার q, r, s বেছে নেয়; theory বলে y > 5 ∧ y < 2 অসম্ভব, শেখা clause (¬q ∨ ¬s). এখন কাঠামোটি UNSAT, তাই F unsatisfiable. এই ভাগাভাগির নাম DPLL(T): SAT অংশ যুক্তির কাঠামো খোঁজে, theory অংশ শুধু atom-এর ∧ যাচাই করে। Bit-vector-এ আরেকটি পথ bit-blasting: w-বিটের প্রতিটি অপারেশনকে Boolean circuit-এ (যেমন adder) ভেঙে CNF বানানো, ঠিক পর্ব ৬৯-এর Boolean function-এর মতো। Two’s complement আর adder-এর হার্ডওয়্যার দিক Computer Architecture কোর্সের পর্ব ২০-এ।

সত্যিকারের run ২: bit-trick আর binary search-এর মাঝখান

Programmer-দের প্রিয় কৌশল x & (x - 1): x-এর সবচেয়ে ডানের 1-বিটটি মুছে দেয় (যেমন 40 = 101000 থেকে 32 = 100000 হয়)। আর x & -x শুধু সেই বিটটি রাখে। Python দিয়ে কয়েক হাজার মান পরীক্ষা করা যায়, কিন্তু 32-বিটে মান 2³²টি, প্রায় ৪৩০ কোটি। Z3 সবগুলোর জন্য একবারে উত্তর দেয়। prove(P) ভেতরে ¬P-এর model খোঁজে: না পেলে “proved”, পেলে সেটিই counterexample (পর্ব ০৭)।

from z3 import BitVec, BitVecVal, ZeroExt, Extract, LShR, ULE, Or, And, Implies, prove

x = BitVec("x", 32)                      # a 32-bit machine word

# x & (x - 1) clears the lowest 1-bit; x & -x keeps only that bit
print("1 clear lowest bit :", end=" "); prove(x & (x - 1) == x - (x & -x))

# power-of-two tests against the definition "x == 2^k for some k"
is_pow2 = Or([x == BitVecVal(1 << k, 32) for k in range(32)])
print("2 pow2 with x != 0 :", end=" "); prove(And(x != 0, x & (x - 1) == 0) == is_pow2)
print("3 pow2 without it  :", end=" "); prove((x & (x - 1) == 0) == is_pow2)

# binary-search midpoint on unsigned 32-bit indices
lo, hi = BitVec("lo", 32), BitVec("hi", 32)
exact = Extract(31, 0, LShR(ZeroExt(1, lo) + ZeroExt(1, hi), 1))   # 33-bit sum: no overflow
print("4 (lo + hi) / 2    :", end=" "); prove(Implies(ULE(lo, hi), LShR(lo + hi, 1) == exact))
print("5 lo + (hi - lo)/2 :", end=" "); prove(Implies(ULE(lo, hi), lo + LShR(hi - lo, 1) == exact))

$ uv run python bit_tricks.py
1 clear lowest bit : proved
2 pow2 with x != 0 : proved
3 pow2 without it  : counterexample
[x = 0]
4 (lo + hi) / 2    : counterexample
[hi = 4294967295, lo = 1]
5 lo + (hi - lo)/2 : proved

লাইন ১: মোছার কৌশল সব 32-বিট x-এ সঠিক। লাইন ২–৩: “x ≠ 0 আর x & (x − 1) = 0” ঠিক তখন, যখন x 2-এর একটি ঘাত; শর্ত x ≠ 0 বাদ দিলে Z3 সঙ্গে সঙ্গে x = 0 দেখায়, কারণ 0 & (−1) = 0 অথচ 0 কোনো 2^k নয়। লাইন ৪ বিখ্যাত bug: binary search-এ (lo + hi) / 2. lo = 1, hi = 4294967295 (= 2³² − 1) নিলে যোগফল 2³², যা 32 বিটে উপচে 0 হয়, আর “মাঝখান” আসে 0, অথচ আসল মাঝখান 2147483648. লাইন ৫-এর lo + (hi - lo) / 2 সব lo ≤ hi-তে সঠিক। লক্ষ করুন “আসল মাঝখান” লিখতে 33 বিটে বড় করা হয়েছে (ZeroExt), যাতে তুলনাটাই উপচে না পড়ে।

৭ · Program যাচাই — overflow আর bounded model checking

সত্যিকারের run ৩: ৮-বিটের overflow-check

৮-বিটের signed পূর্ণসংখ্যা −128 থেকে 127. যন্ত্রে a + b উপচে পড়লে mod 256-এ ঘুরে যায়: 100 + 50 = 150, যা signed-এ −106 পড়া হয়। কোডে প্রায়ই তিন রকম পরীক্ষা দেখা যায়; Z3-কে জিজ্ঞেস করি কোনটি “সত্যিকারের overflow”-এর সমান, যেখানে সত্যিকারের যোগফল 16 বিটে হিসাব করা হয় (SignExt দিয়ে বড় করে নিয়ে)।

from z3 import BitVec, SignExt, And, Or, prove

a, b = BitVec("a", 8), BitVec("b", 8)    # signed 8-bit: -128 .. 127
s = a + b                                # what the machine computes (wraps mod 256)
wide = SignExt(8, a) + SignExt(8, b)     # the true sum, in 16 bits
really_overflows = Or(wide > 127, wide < -128)

naive = And(a > 0, b > 0, s < 0)                       # only checks one direction
textbook = Or(And(a > 0, b > 0, s < 0), And(a < 0, b < 0, s >= 0))
xor_trick = ((s ^ a) & (s ^ b)) < 0                    # sign of result differs from both

for name, check in [("naive", naive), ("textbook", textbook), ("xor trick", xor_trick)]:
    print(f"{name:9}:", end=" ")
    prove(check == really_overflows)

$ uv run python overflow8.py
naive    : counterexample
[b = 191, a = 189]
textbook : proved
xor trick: proved

Z3 bit-vector-এর মান unsigned হিসেবে ছাপে: a = 189 মানে signed-এ 189 − 256 = −67, b = 191 মানে −65. আসল যোগফল −132 < −128, অর্থাৎ overflow; যন্ত্রে 380 mod 256 = 124, একটি ধনাত্মক সংখ্যা। “naive” পরীক্ষা শুধু দুটি ধনাত্মক সংখ্যার উপচে পড়া দেখে, ঋণাত্মক দিকটি ভুলে যায়। বাকি দুটি সব 65,536টি জোড়ায় সঠিক প্রমাণিত। XOR কৌশলের যুক্তি: overflow ঘটে ঠিক তখন, যখন a আর b-এর চিহ্ন এক কিন্তু ফলের চিহ্ন আলাদা; তখন s ⊕ a আর s ⊕ b দুটোরই চিহ্ন-বিট 1. 65,536টি জোড়া একটি লুপেও পরীক্ষা করা যায়; কিন্তু 64 বিটে 2¹²⁸টি জোড়া কোনো লুপে সম্ভব নয়, অথচ Z3-এর প্রশ্ন একই থাকে।

Model checking আর bounded model checking

বাজারঘরের গুদামে একটি পণ্যের স্টক ৮-বিটের unsigned সংখ্যা, শুরুতে 5. প্রতিটি ধাপে 1 থেকে 3 পিসের একটি অর্ডার আসে; স্টক যথেষ্ট হলে তা কাটা হয়। নিরাপত্তার দাবি: স্টক কখনো 5-এর বেশি হবে না (মাল আসে না, তাই বাড়ার কথা নয়)। এমন ব্যবস্থা একটি state machine: অবস্থা s, শুরুর শর্ত I(s), এক ধাপের সম্পর্ক T(s, s′), আর “খারাপ” অবস্থা Bad(s). Model checking মানে যাচাই করা যে শুরু থেকে কোনো খারাপ অবস্থায় পৌঁছানো যায় না; অবস্থার graph-এ এটি একটি reachability প্রশ্ন (পর্ব ৫৪)।

এর প্রমাণ সংজ্ঞা থেকেই: model মানে s₀, …, s_k-এর এমন মান যারা শুরুর শর্ত আর প্রতিটি ধাপ মানে, আর অন্তত একটি খারাপ, অর্থাৎ ঠিক একটি দৈর্ঘ্য ≤ k-এর খারাপ পথ। কিন্তু UNSAT শুধু বলে “k ধাপের মধ্যে নেই”. সব ধাপের জন্য লাগে পর্ব ১৩-এর loop invariant-এর মতো একটি inductive invariant J: (১) I(s) → J(s), (২) J(s) ∧ T(s, s′) → J(s′), (৩) J(s) → ¬Bad(s). তাহলে induction-এ প্রতিটি পৌঁছানো অবস্থায় J সত্য, তাই কোনোটি খারাপ নয়।

সত্যিকারের run ৪: স্টকের লুপে bug খোঁজা

দুটি সংস্করণ: ভুলটিতে শর্ত stock - q >= 0, যা unsigned সংখ্যায় সবসময় সত্য (unsigned বিয়োগের ফল কখনো ঋণাত্মক নয়, বরং ঘুরে যায়); ঠিকটিতে q <= stock.

from z3 import BitVec, BitVecVal, If, ULE, UGT, UGE, And, Or, Not, Solver, sat, unsat

# stock (unsigned 8-bit) starts at 5; each step an order of q in 1..3 arrives
def step(stock, q, buggy):
    ok = UGE(stock - q, 0) if buggy else ULE(q, stock)   # unsigned: first is always true
    return If(ok, stock - q, stock)

def bmc(buggy, k_max):
    for k in range(1, k_max + 1):
        st = [BitVecVal(5, 8)]
        qs = [BitVec(f"q{i}", 8) for i in range(k)]
        s = Solver()
        for q in qs:
            s.add(UGT(q, 0), ULE(q, 3))
            st.append(step(st[-1], q, buggy))
        s.add(Or([UGT(x, 5) for x in st]))              # bad state: stock above 5
        if s.check() == sat:
            m = s.model()
            trace = [m.eval(x).as_long() for x in st]
            return f"bug at depth {k}: orders {[m[q].as_long() for q in qs]}, stock {trace}"
    return f"no bug up to depth {k_max}"

print("buggy guard :", bmc(True, 10))
print("fixed guard :", bmc(False, 10))

# induction: invariant stock <= 5 holds initially and survives one step
x, q = BitVec("x", 8), BitVec("q", 8)
s = Solver()
s.add(ULE(x, 5), UGT(q, 0), ULE(q, 3), Not(ULE(step(x, q, False), 5)))
print("fixed guard, all depths:", "invariant proved" if s.check() == unsat else s.model())

$ uv run python bmc_stock.py
buggy guard : bug at depth 2: orders [3, 3], stock [5, 2, 255]
fixed guard : no bug up to depth 10
fixed guard, all depths: invariant proved

ভুল সংস্করণে BMC দ্বিতীয় ধাপেই bug পেল: 3 পিস কাটলে স্টক 2, তারপর আবার 3 পিসের অর্ডার, শর্ত সত্য, আর 2 − 3 ঘুরে 255. হঠাৎ গুদামে ২৫৫টি “পণ্য”! ঠিক সংস্করণে ১০ ধাপ পর্যন্ত কিছু পাওয়া যায়নি, যা নিজে প্রমাণ নয়। শেষ লাইন J = (stock ≤ 5) inductive কি না পরীক্ষা করে: J সত্য এমন যেকোনো অবস্থা থেকে এক ধাপ পরেও J সত্য (UNSAT মানে কোনো counterexample নেই)। শুরুতে 5 ≤ 5, তাই শর্ত (১)-ও সত্য, আর J নিজেই দাবিটি; তিন শর্ত মিলে সব ধাপের প্রমাণ। ধাপ k বাড়িয়ে এই induction-কে শক্তিশালী করার পদ্ধতিকে k-induction বলে।

৮ · বাস্তবে SAT আর SMT — আর তার সীমা

Model checking-এর ধারণার জন্য Edmund Clarke, E. Allen Emerson আর Joseph Sifakis ২০০৭ সালের Turing Award পান। SAT দিয়ে bounded model checking প্রস্তাব করেন Biere, Cimatti, Clarke আর Zhu, ১৯৯৯ সালের একটি প্রবন্ধে বলে উল্লেখ করা হয়। কয়েকটি ব্যবহার, যতটা প্রকাশ্যে নথিভুক্ত:

• হার্ডওয়্যার: processor-এর নকশায় equivalence checking (দুটি circuit সব ইনপুটে একই ফল দেয় কি না) আর BMC বহুল প্রচলিত বলে বর্ণিত; ১৯৯৪ সালের একটি বহুল আলোচিত processor-এর ভাগের bug-এর পর শিল্পে formal যাচাইয়ের আগ্রহ বাড়ে বলে প্রায়ই বলা হয়।
• Package-এর নির্ভরতা: “এই package-গুলো একসঙ্গে বসানো যায় কি, সংস্করণের শর্ত মেনে?” প্রশ্নটি সাধারণভাবে NP-complete, আর কিছু Linux distribution-এর package manager ও কিছু development tool এর জন্য SAT solver বা SAT-ভিত্তিক পদ্ধতি ব্যবহার করে বলে তাদের নথিতে বলা আছে।
• সফটওয়্যার আর cloud: Z3 নিজে Microsoft Research-এ তৈরি, আর তার পরীক্ষা-তৈরির (test generation) ও driver যাচাইয়ের গবেষণায় ব্যবহারের কথা প্রকাশিত। Amazon Web Services-এর গবেষকরা access-policy বিশ্লেষণে SMT ব্যবহারের পদ্ধতি নিয়ে প্রবন্ধ প্রকাশ করেছেন।

সীমাগুলোও স্পষ্ট বলা দরকার। (১) Undecidability: “এই প্রোগ্রাম কখনো খারাপ অবস্থায় যাবে কি না” সাধারণভাবে অনির্ণেয় (পর্ব ৭৫-এর halting problem আর Rice-এর উপপাদ্য)। BMC এড়িয়ে যায় ধাপ সীমিত করে, invariant এড়িয়ে যায় মানুষের অন্তর্দৃষ্টি চেয়ে। (২) Specification: solver শুধু লেখা দাবি প্রমাণ করে; দাবি ভুল হলে প্রমাণ অর্থহীন। (৩) মডেল আর বাস্তব: ℤ না 32-বিট, compiler-এর আচরণ, সমান্তরাল thread: মডেলে যা নেই, প্রমাণেও তা নেই। (৪) খরচ: §৪ দেখিয়েছে ছোট সূত্রও কঠিন হতে পারে, তাই timeout আর “unknown” বাস্তবের অংশ।

৯ · পরীক্ষার অঙ্ক আর একটি ভুল প্রমাণ

অঙ্ক ১: encoding-এর গণনা

(ক) Petersen graph (১০টি vertex, ১৫টি edge)-এর 3-coloring-এর CNF-এ কয়টি variable আর clause? (খ) PHP¹¹₁₀-এ কয়টি?

1. (ক) variable nk = 10 · 3 = 30; clause n + n·C(3, 2) + m·k = 10 + 30 + 45 = 85.
2. (খ) variable 10 · 11 = 110; clause 11 + 10 · C(11, 2) = 11 + 550 = 561, §৪-এর সত্যিকারের run-এর সঙ্গে মেলে। (দুটিই scratch-এ মেলানো।)

অঙ্ক ২: DPLL শুধু unit দিয়ে

(p) ∧ (¬p ∨ q) ∧ (¬q ∨ r) ∧ (¬r ∨ ¬p ∨ s)-এ DPLL চালান।

1. (p) unit: p = T. দ্বিতীয় clause থেকে ¬p মুছে (q): q = T. তৃতীয় থেকে (r): r = T.
2. চতুর্থ থেকে ¬r আর ¬p মুছে (s): s = T. সব clause সত্য, কোনো অনুমান লাগেনি। Brute force-এ ১৬টি সারির মধ্যে model ঠিক একটি, p = q = r = s = T.

অঙ্ক ৩: 2-SAT হাতে

(x ∨ y) ∧ (¬x ∨ y) ∧ (x ∨ ¬y) ∧ (¬x ∨ ¬y) কি satisfiable?

1. Edge: ¬x→y, ¬y→x; x→y, ¬y→¬x; ¬x→¬y, y→x; x→¬y, y→¬x.
2. x → y → ¬x আর ¬x → y → x: x আর ¬x একই SCC-তে, তাই UNSAT (চারটি clause মিলে দুই variable-এর চারটি সারির প্রতিটিকে বাদ দেয়; brute force-এ মেলানো)।

প্রমাণের ভুল ধরুন: “3-SAT-ও সহজ”

একজন লিখলেন: “প্রতিটি 3-clause (a ∨ b ∨ c)-কে (a ∨ b) ∧ (b ∨ c)-এ ভাঙুন। ফল একটি 2-CNF, যা §৫ অনুযায়ী রৈখিক সময়ে মেলে। তাই 3-SAT polynomial, আর P = NP. ∎”

ভুল কোথায়: রূপান্তরটি সমতুল্য নয়, এমনকি equisatisfiable-ও নয়। a = F, b = F, c = T-তে (a ∨ b ∨ c) সত্য, অথচ (a ∨ b) মিথ্যা: একটি satisfiable 3-CNF ভাঙা রূপে UNSAT হয়ে যেতে পারে। Reduction-এর প্রমাণে সবসময় দুই দিক দেখাতে হয় (উপপাদ্য ৩.২-এর মতো)। সঠিক তথ্য: সহায়ক variable দিয়ে যেকোনো CNF-কে 3-CNF-এ নেওয়া যায়, কিন্তু 2-CNF-এ নয়, যদি না P = NP.

১০ · AI-এর যুগে — encoding আর solver-এর উত্তর যাচাই

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

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

• ছোট উদাহরণে encoding-এর model-সংখ্যা brute force-এর সঙ্গে মিলিয়েছি
• Int আর BitVec, signed আর unsigned সঠিক জায়গায় বসেছে
• “proved” আসলে ¬P-এর UNSAT, আর P-টি আমার চাওয়া দাবিই
• Counterexample হাতে হিসাব করে দেখেছি যে সত্যিই দাবি ভাঙে
• Bounded ফলকে সব ধাপের প্রমাণ বলিনি; invariant আলাদা করে দেখেছি
• উপপাদ্যের শর্ত (2-CNF, pure literal) মিলিয়েছি, আর reference মূল উৎসে খুঁজেছি