k-SAT 問題

\(SAT\)是適定性問題的簡稱

假定現在有多個集合，每個集合有\(k\)個元素，存在著相互制約的關係

每個元素僅有取與不取兩種狀態（定為\(0/1\)）

要想滿足所有集合的制約關係，求解可行性與方案，這便是\(k-SAT\)問題

目前可證明在\(k\gt 2\)時此問題為NP完全問題，所以一般只針對\(2-SAT\)問題進行討論

\(2-SAT\)問題即表示每個集合內僅有\(2\)個元素存在制約關係的\(SAT\)問題

求解\(2-SAT\)問題，即求解出一組滿足制約關係的選擇方案（或證明無解）

Example 1

現有三個物品\(a,b,c\)，給出制約關係——

1、\(a,b\)

2、\(b,c\)不能同時選

由這兩個條件構成的問題即為\(2-SAT\)問題，它的每個制約關係只針對兩個元素

改例子可行性顯然（選\(a,b\)或者選\(c\)）

Example 2

現有三個物品\(a,b,c\)，給出制約關係——

1、\(a,b\)必須同時選

2、\(b,c\)必須同時選

3、\(a,c\)不能同時選

明顯，改例子不存在可行解

2-SAT 在圖中的表示

在描述中有提及，\(2-SAT\)問題的每個元素僅存在取或者不取這兩種狀態

這裡我們將取視作\(1\)，不取視作\(0\)

所以對於每個元素\(x\)，可以將其拆成兩個點\(x_0,x_1\)

對於這兩個點，在存在可行解的情況下一定會選到其中一個點

如果答案中取的是\(x_0\)，則表示答案不取元素\(x\)

反之，如果答案中取的是\(x_1\)，則表示答案取了元素\(x\)

接下來就是將兩點之間的“關係”轉化成圖形來表示——邊

對於兩個元素\(x,y\)之間的關係（或單元素與答案之間的關係），可分為以下幾種

• \(x,y\)必須同時選中：表示要麼都選，要麼都不選，所以連邊情況為\(x_1\rightarrow y_1,y_1\rightarrow x_1\)
• \(x,y\)不能同時選中：選了\(x\)就不能選\(y\)，反之亦然，所以連邊情況為\(x_1\rightarrow y_0,y_1\rightarrow x_0\)
• \(x,y\)
  至少選一個：三種情況，\(x/y/x\&y\)，即如果確定其中一個不選，則另一個就必須選，所以連邊情況為\(x_0\rightarrow y_1,y_0\rightarrow x_1\)
• \(x,y\)必選且只能選一個：相互限制，確定選中另一個就不選，確定不選另一個就選中，所以連邊情況為\(x_0\rightarrow y_1,x_1\rightarrow y_0,y_0\rightarrow x_1,y_1\rightarrow x_0\)
• \(x\)必須選：直接連線\(x_0\rightarrow x_1\)，強制選擇

然後對圖進行處理，即可開始求解問題

2-SAT 的 SCC 解法

主要靠建邊後尋找強連通分量，縮點後確定可行解的方式求解

如果對於某個元素\(x\)，其\(x_0\)與\(x_1\)若在同一強連通分量內（可互相到達），則會造成條件衝突，顯然無解

否則，縮點後圖將會變成一張DAG，那就根據拓撲序，選擇\(x_0\)與\(x_1\)中拓撲序較大的作為選擇狀態即可

此方法常用於判斷可行性，少用於求可行解

時間複雜度為\(O(n+m)\)

例題

HDU 3062 - Party

題意

每對夫妻只能選擇一人蔘加聚會，但由於某些人之間存在矛盾，不能同時讓他們參加聚會，問是否存在一種方案使得聚會能夠有\(n\)個人參加（即每對夫妻都能有一人蔘加）

解

顯然，兩夫妻如果其中一個不參加，另外一個就會參加（假定先不考慮衝突）

所以可以將一對夫妻看作是一個元素的\(x_0\)與\(x_1\)這兩種情況，合法解下為二選一狀態，正好也符合了題意

所以直接根據\(2-SAT\)的建圖法進行建圖，將有矛盾的兩人（兩點\(x,y\)）對應連邊，符合“不能同時選中”的情況，所以建圖方式為\(x_1\rightarrow y_0,y_1\rightarrow x_0\)

跑SCC縮點，最後判斷是否存在一對\(\{x_0,x_1\}\)是在同一個SCC內的即可，如果存在則無解，不存在則有解

#include<bits/stdc++.h>
using namespace std;
const int maxn=2050,maxm=4000050,maxk=10050;

struct Edge
{
    int to,next;
}eg[maxm];
int pre[maxn],lowlink[maxn],sccno[maxn],head[maxn];
int STACK[maxk],STACKTop;
int dfs_clock,scc_cnt,tot;
bool ins[maxn];

inline void SPush(int a)
{
    STACK[STACKTop++]=a;
}
inline void SPop()
{
    STACKTop--;
}
inline bool SEmpty()
{
    return STACKTop==0;
}
inline int STop()
{
    return STACK[STACKTop-1];
}
void init(int nn)
{
    dfs_clock=scc_cnt=STACKTop=tot=0;
    memset(head,-1,(nn<<2)+5);
    memset(sccno,0,(nn<<2)+5);
    memset(pre,0,(nn<<2)+5);
    memset(ins,false,(nn<<2)+5);
}
void addedge(int u,int v)
{
    eg[tot].to=v;
    eg[tot].next=head[u];
    head[u]=tot++;
}
void tarjan(int in)
{
    pre[in]=lowlink[in]=++dfs_clock;
    SPush(in);
    ins[in]=true;
    for(int i=head[in];i!=-1;i=eg[i].next)
    {
        int &v=eg[i].to;
        if(!pre[v])
        {
            tarjan(v);
            lowlink[in]=min(lowlink[in],lowlink[v]);
        }
        else if(ins[v])
            lowlink[in]=min(lowlink[in],pre[v]);
    }
    if(lowlink[in]==pre[in])
    {
        scc_cnt++;
        while(1)
        {
            int x=STop();
            SPop();
            sccno[x]=scc_cnt;
            ins[x]=false;
            if(x==in)
                break;
        }
    }
}

int n;
void solve()
{
    int m,a1,a2,c1,c2;
    scanf("%d",&m);
    init(n<<1);
    for(int i=1;i<=m;i++)
    {
        scanf("%d%d%d%d",&a1,&a2,&c1,&c2);
        a1=a1<<1|c1;
        a2=a2<<1|c2;
        addedge(a1,a2^1);
        addedge(a2,a1^1);
    }
    for(int i=0;i<(n<<1);i++)
    {
        if(!pre[i])
            tarjan(i);
    }
    for(int i=0;i<n;i++)
    {
        if(sccno[i<<1]==sccno[i<<1|1])
        {
            puts("NO");
            return;
        }
    }
    puts("YES");
}
int main()
{
    while(scanf("%d",&n)!=EOF)
        solve();
    return 0;
}

2-SAT 的 DFS 解法

還沒學呢晚上補