關於 SAT

SAT 問題是適定性（Satisfiability）問題的簡稱。中文是所謂的 k-適定性問題，也就是 k-SAT。

這種問題的定義非常簡單：

給定布林變數集合，每個變數只能賦值為真假，要求對每個變數賦值滿足一個布林方程。

可能比較抽象，其實可以理解為有 bool 變數的集合 \(\mathbb B=\{a_1,a_2,a_3,\dots,a_n\}\)

要求求出

\[\begin{aligned} (\neg a_1\or a_2\or\neg a_3&\dots\or a_n)\and(a_1\or a_2\or \neg a_3\dots\or \neg a_n)\and\cdots=1\\ &\Downarrow\\ &\begin{cases} \neg a_1\or a_2\or\neg a_3\dots\or a_n=1\\ a_1\or a_2\or \neg a_3\dots\or \neg a_n=1\\ \vdots \\ \end{cases} \end{aligned} \]

這樣形式的一個方程的解。

實際上，雖然集合元素達到有 \(n\) 個之多，但是我們的限制條件，也就是所謂的括號內單個的布林方程不一定會關係到整個集合的所有元素。我們假設對於每一個括號內獨立的方程存在一個布林集合對映 \(\mathbb S_i\in\mathbb B\)。那麼如果這些子集的元素個數都為 \(k\)（每個 clause 選取 \(k\) 個變數），那麼我們認為這就構成了一個 \(k\) 適定性問題。

沒有理解沒有關係，因為 k-SAT 不考（霧）。

對於這樣一個問題，我們顯然可以暴力賦值解決。

而且當這個問題的 \(k\) 滿足 \(k\geq 3\) 時，被證明為一個 NP-Complete 問題，只能暴力解決。

但是當 \(k=2\) 時，也就是對應方程組中的每一個方程只為二元方程時，我們稱之為 2-SAT 問題，這類問題是可以構建模型利用 \(\texttt{Tarjan}\) 演算法線上性時間內解決的。

---

怎麼解決 2-SAT

問題轉化

之前沒有理解 k-SAT 沒有關係，我們現在以一種通俗的方式重新定義 2-SAT 問題。

對於每個變數我們將其看作一個集合 \(\mathbb A_i=\{\texttt{true,false}\}\)。給定若干個矛盾關係 \(<a,b>\) 表示 \(a,b\) 元素矛盾（\(a,b\) 來自不同集合）。現在要求求出一種可行解使得每個集合只選擇一個元素（共 \(n\)

個）且這些元素之間互無矛盾關係。

我們發現這類問題也可以通過列前文所述的布林方程組解決。

---

模型建立

對於這類問題，我們不難想到建立圖論模型解決。

兩兩布林變數間的邏輯關係可以有多種，但實際上我們可以在 2-SAT 問題中將他們規約成 3 種關係。

• \(\neg a\or b\)
• \(a\or b\)
• \(\neg a\or \neg b\)

對於我們的 \(\or\) 運算，我們容易得到如果左邊不成立則右邊必須成立。所以對於 \(a,b,\neg a,\neg b\) 的狀態我們用四個不同節點 \(T_a,T_b,F_a,F_b\) 表示。

對於第一個式子，當選取 \(a\) 時我們必須選 \(b\)，如果選取 \(\neg b\) 時則必須選取 \(\neg a\)

下面兩式同理。

所以現在我們得到一種依賴關係，可以建圖了。

\(\neg a\or b\)	\(T_a\rightarrow T_a,F_b\rightarrow F_a\)
\(a\or b\)	\(F_a\rightarrow T_b,F_b\rightarrow T_a\)
\(\neg a\or \neg b\)	\(T_a\rightarrow F_b,T_b\rightarrow F_b\)

現在假設我們有依賴關係 \((\neg a\or \neg b)\and(\neg c\or a)\and(c\or\neg b)\)

依照上面方法我們可以得到

這樣的一個圖。

我們觀察發現，這個圖並非連通的有向圖。所以對於每個點的情況都可以找到對應的依賴，也就是說，他是有解的。

如果我們給出一個明顯的無解的依賴關係：\((\neg a\or b)\and(\neg a\or\neg b)\and(a\or b)\and(a\or \neg b)\)

我們構建出來的圖長這樣：

我們發現，對於一個變數 \(a\) 或 \(b\)，他們的其中一值的依賴物件可以達到另一個取值。這樣就會出現無解的情況。其實這是一個很容易去感謝理解的點。畢竟當對於一個布林變數要求到其取 \(2\) 個值的時候，就一定是無解。

那麼轉換一下我們發現，當一個變數的 \(2\) 個邏輯值的代表節點在同一個強連通分量時，這個 2-SAT 問題就是無解的。

---

尋找方案

其實模型建立出來了，找方案只需要一句話即可。

我們可以通過判斷每個點 \(2\) 個取值節點所在的強連通分量的拓撲序即可。

由於拓撲序靠後必然不影響拓撲序靠前的節點，所以對於每個變數我們選擇拓撲序更大的節點對應的邏輯值。

不過對於 \(\texttt{Tarjan}\) 來說，由於棧的使用，拓撲序順序是相反的，實現時需要注意，不過一般來說自己通過樣例試驗一下哪個是對的即可。

---

實現

參考模板題 Luogu P4782 【模板】2-SAT 問題

#include<bits/stdc++.h>

#define INL inline
#define ll long long
#define ull unsigned long long


INL int read()
{
	int x=0,w=1;char ch=getchar();
	while((ch<'0'||ch>'9')&&ch!='-')ch=getchar();
	if(ch=='-')ch=getchar(),w=-1;
	while(ch>='0'&&ch<='9')x=(x<<1)+(x<<3)+ch-48,ch=getchar();
	return x*w;
}

const int N=1e6+5;

struct Rey{int nxt,to;}e[N<<1];
int head[N<<1],cnt;

INL void add(int u,int v)
{
	e[++cnt].nxt=head[u];
	e[cnt].to=v;
	head[u]=cnt;
}

int dfn[N<<1],low[N<<1],col[N<<1],secs,tot;
int n,m;
bool in_stk[N<<1];
std::stack <int> stk;

INL void Tarjan(int x)
{
	dfn[x]=low[x]=++tot;
	stk.push(x);
	in_stk[x]=1;
	for(int i=head[x];i;i=e[i].nxt)
	{
		int v=e[i].to;
		if(!dfn[v])
		{
			Tarjan(v);
			low[x]=std::min(low[x],low[v]);
		}
		else 
			if(in_stk[v])
				low[x]=std::min(low[x],dfn[v]);
	}
	if(dfn[x]==low[x])
	{
		secs++;
		int tp;
		do
		{
			tp=stk.top();
			stk.pop();
			in_stk[tp]=0;
			col[tp]=secs; 
		}while(tp!=x);
	}
}

int main()
{
	//freopen(".in","r",stdin);
	//freopen(".out","w",stdout);
	n=read(),m=read();
	for(int i=1,u,v,a,b;i<=m;i++)
	{
		u=read(),a=read(),v=read(),b=read();
		if(!a&&!b){add(u+n,v);add(v+n,u);}
		else if(!a&&b){add(u+n,v+n);add(v,u);}
		else if(!b&&a){add(u,v);add(v+n,u+n);}
		else if(a&&b){add(u,v+n);add(v,u+n);}
	}
	n<<=1;
	for(int i=1;i<=n;i++)if(!dfn[i])Tarjan(i);
	n>>=1;
	for(int i=1;i<=n;i++)if(col[i]==col[i+n]){puts("IMPOSSIBLE");return 0;}
	puts("POSSIBLE");
	for(int i=1;i<=n;i++)
		if(col[i]>col[i+n])
			printf("1 ");
		else
			printf("0 ");
	return 0;
}

彩蛋：

---

\[\text{2-SAT}\texttt{——2021.06.24} \text{寫在膝上型電腦前} \]

---

Reference:

• \(\text{Anguei}\) - 題解 P4782 【【模板】2-SAT 問題】