২-স্যাট#
SAT (বুলিয়ান স্যাটিসফায়াবিলিটি প্রবলেম) হলো একটি প্রদত্ত বুলিয়ান ফর্মুলা সিদ্ধ করার জন্য ভেরিয়েবলগুলোতে বুলিয়ান মান অ্যাসাইন করার সমস্যা। বুলিয়ান ফর্মুলাটি সাধারণত CNF (কনজাঙ্কটিভ নর্মাল ফর্ম)-এ দেওয়া থাকে, যা একাধিক ক্লজের কনজাঙ্কশন, যেখানে প্রতিটি ক্লজ হলো লিটারেলগুলোর (ভেরিয়েবল বা ভেরিয়েবলের নেগেশন) ডিসজাঙ্কশন। ২-স্যাট (২-স্যাটিসফায়াবিলিটি) হলো SAT সমস্যার একটি সীমাবদ্ধতা, ২-স্যাটে প্রতিটি ক্লজে ঠিক দুটি লিটারেল থাকে। এখানে এরকম একটি ২-স্যাট সমস্যার উদাহরণ দেওয়া হলো। এমন $a, b, c$-এর অ্যাসাইনমেন্ট বের করুন যেন নিম্নলিখিত ফর্মুলাটি সত্য হয়:
$$(a \lor \lnot b) \land (\lnot a \lor b) \land (\lnot a \lor \lnot b) \land (a \lor \lnot c)$$SAT হলো NP-complete, এর জন্য কোনো পরিচিত দক্ষ সমাধান নেই। তবে ২-স্যাট $O(n + m)$ সময়ে দক্ষভাবে সমাধান করা যায় যেখানে $n$ হলো ভেরিয়েবলের সংখ্যা এবং $m$ হলো ক্লজের সংখ্যা।
অ্যালগরিদম:#
প্রথমে আমাদের সমস্যাটিকে একটি ভিন্ন রূপে রূপান্তর করতে হবে, যাকে ইমপ্লিকেটিভ নর্মাল ফর্ম বলা হয়। লক্ষ্য করুন $a \lor b$ রাশিটি $\lnot a \Rightarrow b \land \lnot b \Rightarrow a$ এর সমতুল্য (যদি দুটি ভেরিয়েবলের একটি মিথ্যা হয়, তাহলে অন্যটি অবশ্যই সত্য)।
এখন আমরা এই ইমপ্লিকেশনগুলোর একটি ডিরেক্টেড গ্রাফ তৈরি করি: প্রতিটি ভেরিয়েবল $x$-এর জন্য দুটি ভার্টেক্স $v_x$ এবং $v_{\lnot x}$ থাকবে। এজগুলো ইমপ্লিকেশনের সাথে সঙ্গতিপূর্ণ হবে।
আসুন ২-CNF ফর্মে উদাহরণটি দেখি:
$$(a \lor \lnot b) \land (\lnot a \lor b) \land (\lnot a \lor \lnot b) \land (a \lor \lnot c)$$ওরিয়েন্টেড গ্রাফে নিম্নলিখিত ভার্টেক্স এবং এজ থাকবে:
$$\begin{array}{cccc} \lnot a \Rightarrow \lnot b & a \Rightarrow b & a \Rightarrow \lnot b & \lnot a \Rightarrow \lnot c\\ b \Rightarrow a & \lnot b \Rightarrow \lnot a & b \Rightarrow \lnot a & c \Rightarrow a \end{array}$$আপনি নিম্নলিখিত ছবিতে ইমপ্লিকেশন গ্রাফ দেখতে পারেন:
ইমপ্লিকেশন গ্রাফের বৈশিষ্ট্যটিতে মনোযোগ দেওয়া উচিত: যদি $a \Rightarrow b$ এজ থাকে, তাহলে $\lnot b \Rightarrow \lnot a$ এজও থাকে।
এছাড়াও লক্ষ্য করুন, যদি $x$ থেকে $\lnot x$ পৌঁছানো যায়, এবং $\lnot x$ থেকে $x$ পৌঁছানো যায়, তাহলে সমস্যার কোনো সমাধান নেই। ভেরিয়েবল $x$-এর জন্য আমরা যে মানই বাছাই করি না কেন, এটি সর্বদা একটি দ্বন্দ্বে শেষ হবে — যদি $x$-কে $\text{true}$ অ্যাসাইন করা হয় তাহলে ইমপ্লিকেশন বলে যে $\lnot x$-ও $\text{true}$ হওয়া উচিত এবং বিপরীতভাবে। দেখা যায়, এই শর্তটি শুধু প্রয়োজনীয়ই নয়, যথেষ্টও। আমরা নিচের কয়েকটি অনুচ্ছেদে এটি প্রমাণ করব। প্রথমে স্মরণ করুন, যদি একটি ভার্টেক্স দ্বিতীয়টি থেকে পৌঁছানোযোগ্য হয়, এবং দ্বিতীয়টি প্রথমটি থেকে পৌঁছানোযোগ্য হয়, তাহলে এই দুটি ভার্টেক্স একই স্ট্রংলি কানেক্টেড কম্পোনেন্টে আছে। তাই আমরা সমাধানের অস্তিত্বের মানদণ্ডটি এভাবে প্রণয়ন করতে পারি:
এই ২-স্যাট সমস্যার সমাধান থাকার জন্য, প্রয়োজনীয় ও যথেষ্ট শর্ত হলো যেকোনো ভেরিয়েবল $x$-এর জন্য ভার্টেক্স $x$ এবং $\lnot x$ ইমপ্লিকেশন গ্রাফের স্ট্রং কানেকশনের বিভিন্ন স্ট্রংলি কানেক্টেড কম্পোনেন্টে থাকবে।
এই মানদণ্ডটি সকল স্ট্রংলি কানেক্টেড কম্পোনেন্ট খুঁজে $O(n + m)$ সময়ে যাচাই করা যায়।
নিম্নলিখিত ছবিতে উদাহরণটির সকল স্ট্রংলি কানেক্টেড কম্পোনেন্ট দেখানো হয়েছে। আমরা সহজেই যাচাই করতে পারি যে চারটি কম্পোনেন্টের কোনোটিতেই একটি ভার্টেক্স $x$ এবং এর নেগেশন $\lnot x$ একসাথে নেই, তাই উদাহরণটির একটি সমাধান আছে। পরবর্তী অনুচ্ছেদগুলোতে আমরা শিখব কীভাবে একটি বৈধ অ্যাসাইনমেন্ট গণনা করতে হয়, তবে শুধু প্রদর্শনের জন্য $a = \text{false}$, $b = \text{false}$, $c = \text{false}$ সমাধানটি দেওয়া হলো।
এখন আমরা ২-স্যাট সমস্যার সমাধান খোঁজার অ্যালগরিদম তৈরি করি এই অনুমানে যে সমাধান বিদ্যমান।
লক্ষ্য করুন, সমাধান বিদ্যমান থাকা সত্ত্বেও, ইমপ্লিকেশন গ্রাফে $x$ থেকে $\lnot x$ পৌঁছানোযোগ্য হতে পারে, অথবা (কিন্তু একই সাথে নয়) $\lnot x$ থেকে $x$ পৌঁছানোযোগ্য হতে পারে। সেক্ষেত্রে $x$-এর জন্য $\text{true}$ বা $\text{false}$-এর একটি বাছাই দ্বন্দ্ব তৈরি করবে, অন্যটি করবে না। আসুন শিখি কীভাবে এমন মান বাছাই করতে হয় যেন আমরা দ্বন্দ্ব তৈরি না করি।
আমরা স্ট্রংলি কানেক্টেড কম্পোনেন্টগুলো টপোলজিক্যাল ক্রমে সাজাই (অর্থাৎ $v$ থেকে $u$-তে পাথ থাকলে $\text{comp}[v] \le \text{comp}[u]$) এবং $\text{comp}[v]$ দ্বারা $v$ ভার্টেক্স যে স্ট্রংলি কানেক্টেড কম্পোনেন্টের অন্তর্ভুক্ত তার ইনডেক্স বোঝানো হোক। তাহলে, যদি $\text{comp}[x] < \text{comp}[\lnot x]$ হয় তাহলে আমরা $x$-কে $\text{false}$ অ্যাসাইন করি এবং অন্যথায় $\text{true}$।
আসুন প্রমাণ করি যে ভেরিয়েবলগুলোর এই অ্যাসাইনমেন্টে আমরা দ্বন্দ্বে পৌঁছাই না। ধরুন $x$-কে $\text{true}$ অ্যাসাইন করা হয়েছে। অন্য ক্ষেত্রটি একইভাবে প্রমাণ করা যায়।
প্রথমে আমরা প্রমাণ করি যে ভার্টেক্স $x$ থেকে ভার্টেক্স $\lnot x$ পৌঁছানো সম্ভব নয়। যেহেতু আমরা $\text{true}$ অ্যাসাইন করেছি, তাই $x$-এর স্ট্রংলি কানেক্টেড কম্পোনেন্টের ইনডেক্স $\lnot x$-এর কম্পোনেন্টের ইনডেক্সের চেয়ে বড়। এর মানে $\lnot x$, $x$ ধারণকারী কম্পোনেন্টের বামে অবস্থিত, এবং পরবর্তী ভার্টেক্স থেকে প্রথমটিতে পৌঁছানো সম্ভব নয়।
দ্বিতীয়ত আমরা প্রমাণ করি যে এমন কোনো ভেরিয়েবল $y$ নেই, যেন ইমপ্লিকেশন গ্রাফে $x$ থেকে $y$ এবং $\lnot y$ উভয়ই পৌঁছানোযোগ্য। এটি একটি দ্বন্দ্ব তৈরি করত, কারণ $x = \text{true}$ মানে $y = \text{true}$ এবং $\lnot y = \text{true}$। আসুন পরোক্ষ প্রমাণ করি। ধরুন $y$ এবং $\lnot y$ উভয়ই $x$ থেকে পৌঁছানোযোগ্য, তাহলে ইমপ্লিকেশন গ্রাফের বৈশিষ্ট্য অনুযায়ী $\lnot x$, $y$ এবং $\lnot y$ উভয় থেকে পৌঁছানোযোগ্য। সংক্রমণশীলতা দ্বারা এর ফলে $\lnot x$, $x$ থেকে পৌঁছানোযোগ্য, যা অনুমানের সাথে দ্বন্দ্ব করে।
সুতরাং আমরা এমন একটি অ্যালগরিদম তৈরি করেছি যা ভেরিয়েবলগুলোর প্রয়োজনীয় মান খুঁজে বের করে এই অনুমানে যে যেকোনো ভেরিয়েবল $x$-এর জন্য ভার্টেক্স $x$ এবং $\lnot x$ ভিন্ন স্ট্রংলি কানেক্টেড কম্পোনেন্টে আছে। উপরে এই অ্যালগরিদমের সঠিকতা প্রমাণ করা হয়েছে। ফলস্বরূপ আমরা একই সাথে সমাধানের অস্তিত্বের উপরোক্ত মানদণ্ডটিও প্রমাণ করলাম।
ইমপ্লিমেন্টেশন:#
এখন আমরা সম্পূর্ণ অ্যালগরিদম ইমপ্লিমেন্ট করতে পারি। প্রথমে আমরা ইমপ্লিকেশনের গ্রাফ তৈরি করি এবং সকল স্ট্রংলি কানেক্টেড কম্পোনেন্ট খুঁজি। এটি কোসারাজুর অ্যালগরিদম দিয়ে $O(n + m)$ সময়ে করা যায়। গ্রাফের দ্বিতীয় ট্রাভার্সালে কোসারাজুর অ্যালগরিদম স্ট্রংলি কানেক্টেড কম্পোনেন্টগুলো টপোলজিক্যাল ক্রমে ভিজিট করে, তাই প্রতিটি ভার্টেক্স $v$-এর জন্য $\text{comp}[v]$ গণনা করা সহজ।
এরপর আমরা $\text{comp}[x]$ এবং $\text{comp}[\lnot x]$ তুলনা করে $x$-এর অ্যাসাইনমেন্ট বাছাই করতে পারি। যদি $\text{comp}[x] = \text{comp}[\lnot x]$ হয় তাহলে আমরা $\text{false}$ রিটার্ন করি এটি বোঝাতে যে ২-স্যাট সমস্যা সিদ্ধ করে এমন কোনো বৈধ অ্যাসাইনমেন্ট নেই।
নিচে ইতিমধ্যে তৈরি করা ইমপ্লিকেশনের গ্রাফ $adj$ এবং ট্রান্সপোজ গ্রাফ $adj^{\intercal}$ (যেখানে প্রতিটি এজের দিক উল্টানো হয়েছে) ব্যবহার করে ২-স্যাট সমস্যার সমাধানের ইমপ্লিমেন্টেশন দেওয়া হলো। গ্রাফে $2k$ এবং $2k+1$ ইনডেক্সের ভার্টেক্সগুলো ভেরিয়েবল $k$-এর দুটি ভার্টেক্স, যেখানে $2k+1$ নেগেটেড ভেরিয়েবলের সাথে সঙ্গতিপূর্ণ।
struct TwoSatSolver {
int n_vars;
int n_vertices;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;
TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) {
order.reserve(n_vertices);
}
void dfs1(int v) {
used[v] = true;
for (int u : adj[v]) {
if (!used[u])
dfs1(u);
}
order.push_back(v);
}
void dfs2(int v, int cl) {
comp[v] = cl;
for (int u : adj_t[v]) {
if (comp[u] == -1)
dfs2(u, cl);
}
}
bool solve_2SAT() {
order.clear();
used.assign(n_vertices, false);
for (int i = 0; i < n_vertices; ++i) {
if (!used[i])
dfs1(i);
}
comp.assign(n_vertices, -1);
for (int i = 0, j = 0; i < n_vertices; ++i) {
int v = order[n_vertices - i - 1];
if (comp[v] == -1)
dfs2(v, j++);
}
assignment.assign(n_vars, false);
for (int i = 0; i < n_vertices; i += 2) {
if (comp[i] == comp[i + 1])
return false;
assignment[i / 2] = comp[i] > comp[i + 1];
}
return true;
}
void add_disjunction(int a, bool na, int b, bool nb) {
// na and nb signify whether a and b are to be negated
a = 2 * a ^ na;
b = 2 * b ^ nb;
int neg_a = a ^ 1;
int neg_b = b ^ 1;
adj[neg_a].push_back(b);
adj[neg_b].push_back(a);
adj_t[b].push_back(neg_a);
adj_t[a].push_back(neg_b);
}
static void example_usage() {
TwoSatSolver solver(3); // a, b, c
solver.add_disjunction(0, false, 1, true); // a v not b
solver.add_disjunction(0, true, 1, true); // not a v not b
solver.add_disjunction(1, false, 2, false); // b v c
solver.add_disjunction(0, false, 0, false); // a v a
assert(solver.solve_2SAT() == true);
auto expected = vector<bool>{{true, false, true}};
assert(solver.assignment == expected);
}
};