تشخیص دو صدق‌پذیری

عبارتی بولی مانند $(x0 \lor x1) \land (x3 \lor \lnot x5) \land ( \lnot x1 \lor x4) $ را در نظر بگیرید. این عبارت از 3 بند تشکیل شده‌است که بین بند‌های آن $\land$ وجود دارد. هر بند دو متغیر دارد که بین آن‌ها $\lor$ است. به مسئله تشخیص توانایی درست بودن یک عبارت بولی که از $and$ چند بند که هر بند از $or$ دو متغیر(هر متغیر ممکن است خودش یا نقیضش استفاده شده باشد) تشکیل شده است، مسئله دو صدق‌پذیری می گویند.

ابتدا به ازای هر متغیر یک راس و به ازای نقیض هر متغیر نیز یک راس در نظر می گیریم. حال به ازای هر بند در عبارت بولی مانند $(a \lor b)$ یک یال جهتدار از راس $\lnot a$ به راس $b$ و یک یال جهتدار از راس $\lnot b$ به راس $a$ می‌گذاریم. حال به کمک الگوریتم پیدا کردن مولفه‌های قویا همبند، مولفه های قویا همبند گراف ایجاد شده را بدست می آوریم. اگر متغیری بود که با نقیضش در یک مولفه بود، عبارت بولی نمی تواند جواب نهاییش صحیح باشد. در غیر اینصورت عبارت بولی می تواند مقدارش صحیح باشد.

در گراف ایجاد شده اگر از راس $a$ به راس $b$ مسیر وجود داشته باشد، درست بودن $a$ درست بودن $b$ را نتیجه می دهد (زیرا هر یال از $a$ به $b$ قرار می دهیم این خاصیت را دارد). پس اگر دو راس در یک مولفه قویا همبند باشند مقدار نهایی آن ها برای صحیح بودن مقدار کل باید برابر باشد. پس متغیری با نقیضش نمی‎‌تواند در یک مولفه قویاهمبند باشد. حال اگر هیچ متغیری با نقیضش در یک مولفه قویاهمبند نباشد، می توان به ازای هر متغیر در صورت کمتر بودن شماره‌ی مولفه قویاهمبندش نسبت به شماره‌ی مولفه قویاهمبند نقیضش، مقدار نادرست را به این متغیر بدهیم و در غیراینصورت مقدار صحیح را به این متغیر بدهیم (شماره‌ی مولفه در پیدا کردن مولفه‌های قویا همبند مشخص شده است). در این حالت هیچ دو راسی مانند $a$ و $b$ بوجود نمی‌آید که از $a$ به $b$ مسیر باشد و مقدار $a$ صحیح باشد اما مقدار $b$ صحیح نباشد. زیر اگر اینطوری باشد، آنگاه با توجه به صحیح بودن $a$ شماره مولفه $a$ از $\lnot a$ بیش‎تر است و با توجه به مسیر $a$ به $b$ شماره مولفه $b$ بزرگتر مساوی شماره مولفه $a$ است. همینطور بدلیل صحیح نبودن $b$ شماره مولفه $\lnot b$ از شماره مولفه $b$ بیش‎‌تر است و در نهایت بدلیل مسیر از $a$ به $b$، مسیر از $\lnot b$ به $\lnot a$ وجود دارد که باعث می شود شماره مولفه $\lnot a$ بیش‌تر مساوی شماره مولفه $\lnot b$ شود که تناقض دارد. درنتیجه مقدار دهی گفته شده برای متغیر‌ها خروجی صحیح به عبارت بولی می‌دهد.

فرض کنید تعداد متغیر‌ها $n$ و تعداد بند‌ها $m$ تا باشد. آنگاه ابتدا با $O(n+m)$ گرافی با $2n$ راس و $2m$ یال ساختیم و با $O(n+m)$ مولفه‌های قویا همبند آن را بدست آورده و برای هر متغیر شرط یکسان نبودن مولفه‌ا‌ش با نقیضش را چک کردیم. پس الگوریتم ما در کل دارای مرتبه زمانی $\theta (n+m)$ است.

2SAT.cpp

#include<iostream>
#include<vector>
using namespace std;
 
const int maxn=1e5;
int n, m, comps, comp[maxn];
bool mark[maxn];
vector<int>G[maxn], BG[maxn], myStack;
 
void back_dfs(int v)
{
	comp[v]=comps;
	mark[v]=true;
	for(int i=0;i<BG[v].size();i++)
	{
		int u=BG[v][i];
		if(!mark[u])
			back_dfs(u);
	}
}
 
void dfs(int v)
{
	mark[v]=true;
	for(int i=0;i<G[v].size();i++)
	{
		int u=G[v][i];
		if(!mark[u])
			dfs(u);
	}
	myStack.push_back(v);
}
 
void find_comps()
{
    for(int i=1;i<=2*n;i++)
        if(!mark[i])
            dfs(i);
    fill_n(mark, 2*n+1, false);
    for(int i=myStack.size()-1;i>-1;i--)
        if(!mark[myStack[i]])
        {
            comps++;
            back_dfs(myStack[i]);
        }
}
 
void add_edge(int x,int y)
{
    G[x].push_back(y);
    BG[y].push_back(x);
}
 
int main()
{
    cin>>n>>m;
    for(int i=0;i<m;i++)
    {
        int x,y;// است i به معنای نقیض (n*2-i+1)
        cin>>x>>y;
        add_edge(2*n-x+1,y);
        add_edge(2*n-y+1,x);
    }
    find_comps();
    for(int i=1;i<=n;i++)
        if(comp[i] == comp[2*n-i+1])
        {
            cout<<"NO\n";
            return 0;
        }
    cout<<"YES\n";
}

• http://codeforces.com/gym/100570/problem/D