SAT Solver (DPLL)

কেন এই প্রজেক্ট

আগের দুইটা লেসনে আপনি দেখেছেন SAT NP-complete — শুধু আরেকটা কঠিন সমস্যা না, বরং সেই “প্রথম ইট” যার উপর হাজার হাজার অন্য সমস্যার কাঠিন্য দাঁড়িয়ে (Cook-Levin theorem, reduction transitivity)। কিন্তু তত্ত্বটা জানা আর একটা solver নিজে হাতে বানানো সম্পূর্ণ ভিন্ন অভিজ্ঞতা — কারণ solver বানাতে গেলেই আপনি সরাসরি মুখোমুখি হবেন সেই জিনিসটার যা NP-completeness-এর সংজ্ঞাতেই আড়াল হয়ে থাকে: worst-case exponential হওয়া সত্ত্বেও, বাস্তব instance-এ কেন এত দ্রুত সমাধান পাওয়া যায়?

DPLL (Davis-Putnam-Logemann-Loveland) algorithm — ১৯৬২ সালের, আজও প্রতিটা আধুনিক SAT solver-এর কঙ্কাল — এই প্রশ্নের একটা ব্যবহারিক উত্তর। আপনি দেখবেন কীভাবে দুইটা সরল কৌশল (unit propagation, pure literal elimination) exponential search tree-র বিশাল অংশ কেটে ফেলে দিতে পারে, বিনা কোনো তাত্ত্বিক গ্যারান্টি লঙ্ঘন করে। আর শেষে, random 3-SAT instance-এ benchmark চালিয়ে নিজের চোখে দেখবেন সেই বিখ্যাত “easy-hard-easy” প্যাটার্ন — যেখানে সবচেয়ে কঠিন instance পাওয়া যায় ঠিক সেই বিন্দুতে যেখানে satisfiable আর unsatisfiable instance-এর সংখ্যা প্রায় সমান।

ধাপে ধাপে

১. CNF representation

Clause-দের একটা list হিসেবে রাখুন, প্রতিটা clause literal-দের একটা list (positive int = variable true, negative = variable false):

# (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ x2) ∧ (x3)
clauses = [[1, -2, 3], [-1, 2], [3]]

DIMACS format পার্স করুন (standard SAT competition input format):

def parse_dimacs(text: str) -> tuple[list[list[int]], int]:
    clauses, n_vars = [], 0
    for line in text.splitlines():
        line = line.strip()
        if not line or line.startswith("c"):
            continue
        if line.startswith("p"):
            _, _, nv, _ = line.split()
            n_vars = int(nv)
            continue
        lits = [int(x) for x in line.split() if x != "0"]
        if lits:
            clauses.append(lits)
    return clauses, n_vars

Checkpoint: একটা ছোট হাতে-লেখা DIMACS ফাইল পার্স করে print করুন, লাইন সংখ্যা আর clause সংখ্যা মিলছে কি না দেখুন।

২. Unit propagation

একটা clause-এ যদি ঠিক একটা literal বাকি থাকে (বাকিগুলো ইতিমধ্যে false হয়ে গেছে assignment-এর কারণে), সেই literal-কে বাধ্যতামূলকভাবে true সেট করতে হবে — নাহলে clause-টা unsatisfied হয়ে যাবে।

def unit_propagate(clauses, assignment):
    """assignment: {var: bool}। বদলানো clauses আর assignment ফেরত দেয়,
    conflict হলে None।"""
    changed = True
    while changed:
        changed = False
        for clause in clauses:
            unassigned = [l for l in clause if abs(l) not in assignment]
            if not unassigned:
                # সব literal assigned — satisfied কি না চেক
                if not any((assignment[abs(l)] if l > 0 else not assignment[abs(l)])
                           for l in clause):
                    return None  # conflict — empty/falsified clause
                continue
            if len(unassigned) == 1:
                lit = unassigned[0]
                assignment[abs(lit)] = (lit > 0)
                changed = True
    return assignment

কেন এটা এত গুরুত্বপূর্ণ: বাস্তব CNF formula-য় unit propagation একাই প্রায়ই assignment-এর বড় অংশ নির্ধারণ করে দেয় — কোনো branching (guess) ছাড়াই। এটাকে বলা হয় cascade — একটা variable সেট হলে কিছু clause এক-literal হয়ে যায়, তারা আরেকটা variable সেট করতে বাধ্য করে, চলতেই থাকে।

Checkpoint: একটা “chain” formula বানান যেখানে একটা variable সেট করলে ডমিনো-র মতো বাকি সবগুলো cascade হয়ে সেট হয়ে যায় (যেমন (x1) ∧ (¬x1 ∨ x2) ∧ (¬x2 ∨ x3) ∧ ...) — verify করুন পুরো assignment একটা মাত্র unit_propagate call-এই বের হয়ে যায়, কোনো branching ছাড়া।

৩. Pure literal elimination

যদি একটা variable x পুরো formula-তে সবসময় একই polarity-তে দেখা যায় (শুধু x, কখনো ¬x নয় — বা উল্টো), তাহলে সেটাকে সেই polarity-তে সেট করে দেওয়া নিরাপদ — কোনো clause এতে খারাপ হবে না (কারণ যে clause-গুলোতে এটা আছে, সবগুলোই এই মানে satisfied হয়ে যাবে; যেগুলোতে নেই, তাদের উপর কোনো প্রভাব নেই)।

def pure_literal_eliminate(clauses, assignment):
    counts = {}
    for clause in clauses:
        for lit in clause:
            if abs(lit) not in assignment:
                counts.setdefault(abs(lit), set()).add(lit > 0)
    for var, polarities in counts.items():
        if len(polarities) == 1:  # শুধু এক polarity-তেই দেখা যায়
            assignment[var] = polarities.pop()
    return assignment

Checkpoint: একটা formula বানান যেখানে x5 শুধু positive literal হিসেবে ৪টা clause-এ আছে — pure literal elimination-এর পরে x5 অবশ্যই True সেট হবে, আর সেই ৪টা clause সব satisfied বলে চিহ্নিত হবে, কোনো search ছাড়াই।

৪. DPLL backtracking search

মূল recursive algorithm — unit propagation আর pure literal elimination দিয়ে যতটা সম্ভব সরলীকরণের পর, যদি এখনো অমীমাংসিত variable থাকে, একটা বেছে নিয়ে দুটো branch (true/false) চেষ্টা করুন:

def dpll(clauses, assignment):
    assignment = unit_propagate(clauses, dict(assignment))
    if assignment is None:
        return None  # conflict
    assignment = pure_literal_eliminate(clauses, assignment)

    unassigned = {abs(l) for c in clauses for l in c} - set(assignment)
    if not unassigned:
        return assignment  # সব variable set, কোনো conflict নেই — SAT!

    var = next(iter(unassigned))  # branching heuristic — এখানে সরল, পরে উন্নত করুন
    for value in (True, False):
        new_assignment = dict(assignment)
        new_assignment[var] = value
        result = dpll(clauses, new_assignment)
        if result is not None:
            return result
    return None  # দুটো branch-ই ব্যর্থ — UNSAT এই সাব-ট্রিতে


def solve(clauses):
    result = dpll(clauses, {})
    return result  # None = UNSAT, dict = satisfying assignment

লক্ষ্য করুন কাঠামোটা — এটা এই module-এর “NP-completeness ও Cook-Levin” লেসনের NTM-দৃষ্টির সাথে হুবহু মেলে: প্রতিটা branch একটা computation tree-র node, আর কোনো branch satisfying assignment-এ পৌঁছালেই আমরা “accept” করি। DPLL এই tree-টাকেই prune করে — পুরোটা explore না করেই বড় অংশ বাদ দেয়।

Checkpoint: একটা ছোট (৫-১০ variable) unsatisfiable formula বানিয়ে verify করুন solver None ফেরত দেয়, আর একটা satisfiable formula-য় ফেরত দেওয়া assignment সত্যিই সব clause satisfy করে (একটা independent checker লিখে যাচাই করুন — solver-কেই বিশ্বাস করবেন না)।

৫. Stretch — এক-স্তরের CDCL sketch

আধুনিক solver (MiniSat, CaDiCaL) শুধু backtrack করে না — একটা conflict-এ পৌঁছালে সেই conflict-এর কারণ বিশ্লেষণ করে একটা নতুন clause “শেখে” (learned clause), যা ভবিষ্যতে একই ভুল এড়াতে সাহায্য করে।

def dpll_with_learning(clauses, assignment, learned=None):
    if learned is None:
        learned = []
    all_clauses = clauses + learned

    assignment = unit_propagate(all_clauses, dict(assignment))
    if assignment is None:
        # সরলীকৃত conflict analysis — বর্তমান decision-গুলোর negation-ই
        # একটা বৈধ (যদিও দুর্বল) learned clause
        decided = [(-v if val else v) for v, val in assignment.items()] \
            if assignment else []
        return None, learned  # সম্পূর্ণ CDCL-এ এখানে একটা নতুন clause যোগ হতো

    unassigned = {abs(l) for c in all_clauses for l in c} - set(assignment)
    if not unassigned:
        return assignment, learned

    var = next(iter(unassigned))
    for value in (True, False):
        new_assignment = dict(assignment)
        new_assignment[var] = value
        result, learned = dpll_with_learning(clauses, new_assignment, learned)
        if result is not None:
            return result, learned
    return None, learned

এটা একটা সরলীকৃত sketch — প্রকৃত CDCL implication graph ব্যবহার করে সঠিক learned clause বের করে (1-UIP scheme) আর non-chronological backtracking করে। এখানে লক্ষ্য শুধু ধারণাটা অনুভব করা: conflict থেকে তথ্য বাঁচিয়ে রাখা, প্রতিবার শূন্য থেকে শুরু না করা।

Checkpoint: একটা formula বানান যেখানে একই “ভুল” branching সিদ্ধান্ত বারবার বিভিন্ন সাব-ট্রিতে আসে — plain DPLL কতবার একই conflict-এ পড়ে গণনা করুন, আর ব্যাখ্যা করুন কেন learning এটা কমাতে পারত (সম্পূর্ণ implement করা optional, তাত্ত্বিক ব্যাখ্যাই যথেষ্ট এই checkpoint-এ)।

৬. Random 3-SAT generator ও benchmark

import random

def random_3sat(n_vars, n_clauses, seed=None):
    rng = random.Random(seed)
    clauses = []
    for _ in range(n_clauses):
        vars_chosen = rng.sample(range(1, n_vars + 1), 3)
        clause = [v if rng.random() < 0.5 else -v for v in vars_chosen]
        clauses.append(clause)
    return clauses


import time

def benchmark(n_vars=20, ratios=None, trials=20):
    if ratios is None:
        ratios = [3.0, 3.5, 4.0, 4.2, 4.26, 4.3, 4.5, 5.0, 5.5, 6.0]
    print(f"{'ratio':>6} {'sat%':>6} {'avg_time(ms)':>14} {'max_time(ms)':>14}")
    for ratio in ratios:
        n_clauses = int(n_vars * ratio)
        times, sat_count = [], 0
        for t in range(trials):
            clauses = random_3sat(n_vars, n_clauses, seed=t)
            t0 = time.perf_counter()
            result = solve(clauses)
            dt = (time.perf_counter() - t0) * 1000
            times.append(dt)
            if result is not None:
                sat_count += 1
        print(f"{ratio:>6.2f} {100*sat_count/trials:>5.0f}% "
              f"{sum(times)/len(times):>14.2f} {max(times):>14.2f}")

n_vars = 20-এর কাছাকাছি চালান (বড় হলে plain DPLL অনেক সময় নেবে)।

নিজেকে চ্যালেঞ্জ করুন

Branching heuristic উন্নত করুন — random variable বাছার বদলে “সবচেয়ে বেশি clause-এ আছে এমন variable” (DLIS-এর মতো heuristic) বাছুন, আর runtime-এর উন্নতি measure করুন
সম্পূর্ণ CDCL — implication graph বানিয়ে সঠিক 1-UIP learned clause বের করুন, আর non-chronological backtracking (backjumping) implement করুন
Clause database management — learned clause সংখ্যা বাড়তে থাকলে memory বাড়ে; একটা simple “activity-based” clause deletion policy লিখুন (কম-ব্যবহৃত learned clause সরিয়ে ফেলা)
Watched literals — unit propagation-এর O(n) প্রতি clause-চেক এড়িয়ে, MiniSat-এর “two watched literals” কৌশল দিয়ে propagation দ্রুত করুন
DIMACS competition benchmark — SATLIB বা SAT Competition-এর বাস্তব benchmark ফাইল (public archive) দিয়ে আপনার solver যাচাই করুন, একটা established solver-এর সাথে সময় তুলনা করুন
Reduction demo — আগের লেসনের 3-SAT → Vertex Cover reduction ব্যবহার করে একটা Vertex Cover instance-কে আপনার SAT solver দিয়ে সমাধান করুন (reduce করে solve, তারপর ফলাফল ফিরিয়ে আনুন)

যা এখানে শিখলেন, পরে যেখানে লাগবে

এখানে	পরে
CNF, unit propagation, backtracking	Formal methods module — model checker-এর ভেতরে ঠিক এই একই SAT/SMT ইঞ্জিন চলে
Search tree pruning (DPLL-এর মূল কৌশল)	যেকোনো constraint satisfaction/backtracking algorithm — N-Queens থেকে Sudoku সমাধান পর্যন্ত
Conflict learning (CDCL sketch)	Modern ILP/SMT solver-এর ভেতরের একই ধারণা — Gurobi, Z3
Reduction-চালিত সমস্যা-সমাধান	Package manager dependency resolution (apt, cargo) — আক্ষরিকভাবে SAT সমাধান করছে ভেতরে
“Easy-hard-easy” threshold observation	Random structure-এর phase transition — statistical physics-এর সাথে জটিলতা তত্ত্বের একটা বিখ্যাত সংযোগ

মাইলস্টোন

আগে যা পড়া দরকার