2-可满足性（2-SAT）问题

布尔可满足性问题

布尔可满足性或简称SAT是确定布尔公式是可满足还是不可满足的问题。

可满足：如果可以为布尔变量赋值，使得公式结果为 TRUE，那么我们说该公式是可满足的。
Unsatisfiable ：如果不能分配这样的值，那么我们说这个公式是不可满足的。

例子：

$F = A \wedge \bar{B}$ , 是可满足的，因为 A = TRUE 和 B = FALSE 使得 F = TRUE。
$G = A \wedge \bar{A}$ , 是不可满足的，因为：

$A$	$\bar{A}$	$G$
TRUE	FALSE	FALSE
FALSE	TRUE	FALSE

注意：布尔可满足性问题是 NP 完全的（为了证明，请参阅库克定理）。

布尔可满足性问题

什么是 2-SAT 问题

2-SAT is a special case of Boolean Satisfiability Problem and can be solved
in polynomial time.

编程需要懂一点英语

为了更好地理解这一点，首先让我们看看什么是合取范式 (CNF) 或也称为和积 (POS)。
CNF ： CNF 是子句的合取 (AND)，其中每个子句都是析取 (OR)。
现在，2-SAT 将 SAT 的问题限制为仅表示为 CNF 的那些布尔公式，每个子句只有2 个术语（也称为2-CNF ）。
例子： $F = (A_1 \vee B_1) \wedge (A_2 \vee B_2) \wedge (A_3 \vee B_3) \wedge ....... \wedge (A_m \vee B_m)$
因此，2-可满足性问题可以表述为：
给定 CNF，每个子句只有 2 个术语，是否可以将这些值分配给变量以使 CNF 为 TRUE？
例子：

输入： $F = (x1 \vee x2) \wedge (x2 \vee \bar{x1}) \wedge (\bar{x1} \vee \bar{x2})$ 输出：给定的表达式是可满足的。（对于 x1 = FALSE，x2 = TRUE）输入： $F = (x1 \vee x2) \wedge (x2 \vee \bar{x1}) \wedge (x1 \vee \bar{x2}) \wedge (\bar{x1} \vee \bar{x2})$ 输出：给定的表达式是不可满足的。（对于 x1 和 x2 的所有可能组合）

2-SAT 问题的方法

为了使 CNF 值变为 TRUE，每个子句的值都应为 TRUE。让其中一个子句是 $(A \vee B)$ .
$由 QuickLaTeX.com 渲染$ = 真

如果 A = 0，则 B 必须为 1，即 $(\bar{A} \Rightarrow B)$
如果 B = 0，则 A 必须为 1，即 $(\bar{B} \Rightarrow A)$

因此，

$(A \vee B)$ = TRUE 相当于 $(\bar{A} \Rightarrow B) \wedge (\bar{B} \Rightarrow A)$

现在，我们可以将 CNF 表示为蕴涵。因此，我们创建了一个蕴涵图，它为 CNF 的每个子句都有 2 条边。
$(A \vee B)$ 在蕴涵图中表示为 $edge(\bar{A} \rightarrow B) \ & edge(\bar{B} \rightarrow A)$
因此，对于带有“m”子句的布尔公式，我们制作了一个蕴含图：

每个子句有 2 条边，即“2m”条边。
布尔公式中涉及的每个布尔变量都有 1 个节点。

让我们看一个蕴含图的例子。
$由 QuickLaTeX.com 渲染$

2-SAT 问题的方法

注意：蕴涵（如果 A 那么 B）等价于它的对立面（如果 $\bar{B}$ 然后 $\bar{A}$ ）。
现在，考虑以下情况：

案例 1：如果 $edge(X \rightarrow \bar{X})$ [Tex]存在于图中[/Tex] 这意味着 $(X \Rightarrow \bar{X})$ 如果 X = TRUE， $\bar{X}$ = TRUE，这是一个矛盾。但如果 X = FALSE，则没有隐含约束。因此，X = FALSE

案例 2：如果 $edge(\bar{X} \rightarrow X)$ [Tex]存在于图中[/Tex] 这意味着 $(\bar{X} \Rightarrow X)$ 如果 $\bar{X}$ = TRUE，X = TRUE，这是一个矛盾。但如果 $\bar{X}$ = FALSE，没有隐含约束。因此， $\bar{X}$ = 假，即 X = 真

案例 3：如果 $edge(X \rightarrow \bar{X}) \& edge(\bar{X} \rightarrow X)$ [Tex]两者都存在于图中[/Tex] 一条边要求 X 为 TRUE，另一条边要求 X 为 FALSE。因此，在这种情况下没有可能的分配。

结论：如果任意两个变量 $X$ 和 $\bar{X}$ 是在一个周期，即 $path(\bar{A} \rightarrow B) \& path({B} \rightarrow A)$ 两者都存在，则 CNF 不可满足。否则，有一个可能的分配并且 CNF 是可满足的。
请注意，我们使用路径是由于以下隐含属性：
如果我们有 $(A \Rightarrow B) \& (B \Rightarrow C), then A \Rightarrow C$
因此，如果我们在蕴涵图中有一条路径，那与拥有一条直接边几乎相同。
从实施的角度得出的结论：
如果 X 和 $\bar{X}$ 在同一个 SCC（Strongly Connected Component）中，CNF 是不可满足的。
有向图的强连通分量具有节点，使得每个节点都可以从该 SCC 中的每个其他节点到达。
现在，如果 X 和 $\bar{X}$ 躺在同一个SCC上，我们肯定会有 $path(\bar{A} \rightarrow B) \& path({B} \rightarrow A)$ 现在，因此得出结论。
可以使用 Kosaraju 算法在 O(E+V) 中完成 SCC 的检查

C++

// C++ implementation to find if the given
// expression is satisfiable using the
// Kosaraju's Algorithm
#include 
using namespace std;
 
const int MAX = 100000;
 
// data structures used to implement Kosaraju's
// Algorithm. Please refer
// https://www.geeksforgeeks.org/strongly-connected-components/
vector adj[MAX];
vector adjInv[MAX];
bool visited[MAX];
bool visitedInv[MAX];
stack s;
 
// this array will store the SCC that the
// particular node belongs to
int scc[MAX];
 
// counter maintains the number of the SCC
int counter = 1;
 
// adds edges to form the original graph
void addEdges(int a, int b)
{
    adj[a].push_back(b);
}
 
// add edges to form the inverse graph
void addEdgesInverse(int a, int b)
{
    adjInv[b].push_back(a);
}
 
// for STEP 1 of Kosaraju's Algorithm
void dfsFirst(int u)
{
    if(visited[u])
        return;
 
    visited[u] = 1;
 
    for (int i=0;i b[i]
        // AND -b[i] -> a[i]
        if (a[i]>0 && b[i]>0)
        {
            addEdges(a[i]+n, b[i]);
            addEdgesInverse(a[i]+n, b[i]);
            addEdges(b[i]+n, a[i]);
            addEdgesInverse(b[i]+n, a[i]);
        }
 
        else if (a[i]>0 && b[i]<0)
        {
            addEdges(a[i]+n, n-b[i]);
            addEdgesInverse(a[i]+n, n-b[i]);
            addEdges(-b[i], a[i]);
            addEdgesInverse(-b[i], a[i]);
        }
 
        else if (a[i]<0 && b[i]>0)
        {
            addEdges(-a[i], b[i]);
            addEdgesInverse(-a[i], b[i]);
            addEdges(b[i]+n, n-a[i]);
            addEdgesInverse(b[i]+n, n-a[i]);
        }
 
        else
        {
            addEdges(-a[i], n-b[i]);
            addEdgesInverse(-a[i], n-b[i]);
            addEdges(-b[i], n-a[i]);
            addEdgesInverse(-b[i], n-a[i]);
        }
    }
 
    // STEP 1 of Kosaraju's Algorithm which
    // traverses the original graph
    for (int i=1;i<=2*n;i++)
        if (!visited[i])
            dfsFirst(i);
 
    // STEP 2 of Kosaraju's Algorithm which
    // traverses the inverse graph. After this,
    // array scc[] stores the corresponding value
    while (!s.empty())
    {
        int n = s.top();
        s.pop();
 
        if (!visitedInv[n])
        {
            dfsSecond(n);
            counter++;
        }
    }
 
    for (int i=1;i<=n;i++)
    {
        // for any 2 variable x and -x lie in
        // same SCC
        if(scc[i]==scc[i+n])
        {
            cout << "The given expression "
                 "is unsatisfiable." << endl;
            return;
        }
    }
 
    // no such variables x and -x exist which lie
    // in same SCC
    cout << "The given expression is satisfiable."
         << endl;
    return;
}
 
//  Driver function to test above functions
int main()
{
    // n is the number of variables
    // 2n is the total number of nodes
    // m is the number of clauses
    int n = 5, m = 7;
 
    // each clause is of the form a or b
    // for m clauses, we have a[m], b[m]
    // representing a[i] or b[i]
 
    // Note:
    // 1 <= x <= N for an uncomplemented variable x
    // -N <= x <= -1 for a complemented variable x
    // -x is the complement of a variable x
 
    // The CNF being handled is:
    // '+' implies 'OR' and '*' implies 'AND'
    // (x1+x2)*(x2’+x3)*(x1’+x2’)*(x3+x4)*(x3’+x5)*
    // (x4’+x5’)*(x3’+x4)
    int a[] = {1, -2, -1, 3, -3, -4, -3};
    int b[] = {2, 3, -2, 4, 5, -5, 4};
 
    // We have considered the same example for which
    // Implication Graph was made
    is2Satisfiable(n, m, a, b);
 
    return 0;
}

Java

// Java implementation to find if the given
// expression is satisfiable using the
// Kosaraju's Algorithm
import java.io.*;
import java.util.*;
 
class GFG{
 
static final int MAX = 100000;
 
// Data structures used to implement Kosaraju's
// Algorithm. Please refer
// https://www.geeksforgeeks.org/strongly-connected-components/
@SuppressWarnings("unchecked")
static List > adj = new ArrayList();
 
@SuppressWarnings("unchecked")
static List > adjInv = new ArrayList();
static boolean[] visited = new boolean[MAX];
static boolean[] visitedInv = new boolean[MAX];
static Stack s = new Stack();
 
// This array will store the SCC that the
// particular node belongs to
static int[] scc = new int[MAX];
 
// counter maintains the number of the SCC
static int counter = 1;
 
// Adds edges to form the original graph void
static void addEdges(int a, int b)
{
    adj.get(a).add(b);
}
 
// Add edges to form the inverse graph
static void addEdgesInverse(int a, int b)
{
    adjInv.get(b).add(a);
}
 
// For STEP 1 of Kosaraju's Algorithm
static void dfsFirst(int u)
{
    if (visited[u])
        return;
 
    visited[u] = true;
 
    for(int i = 0; i < adj.get(u).size(); i++)
        dfsFirst(adj.get(u).get(i));
 
    s.push(u);
}
 
// For STEP 2 of Kosaraju's Algorithm
static void dfsSecond(int u)
{
    if (visitedInv[u])
        return;
 
    visitedInv[u] = true;
 
    for(int i = 0; i < adjInv.get(u).size(); i++)
        dfsSecond(adjInv.get(u).get(i));
 
    scc[u] = counter;
}
 
// Function to check 2-Satisfiability
static void is2Satisfiable(int n, int m,
                           int a[], int b[])
{
     
    // Adding edges to the graph
    for(int i = 0; i < m; i++)
    {
         
        // variable x is mapped to x
        // variable -x is mapped to n+x = n-(-x)
 
        // for a[i] or b[i], addEdges -a[i] -> b[i]
        // AND -b[i] -> a[i]
        if (a[i] > 0 && b[i] > 0)
        {
            addEdges(a[i] + n, b[i]);
            addEdgesInverse(a[i] + n, b[i]);
            addEdges(b[i] + n, a[i]);
            addEdgesInverse(b[i] + n, a[i]);
        }
 
        else if (a[i] > 0 && b[i] < 0)
        {
            addEdges(a[i] + n, n - b[i]);
            addEdgesInverse(a[i] + n, n - b[i]);
            addEdges(-b[i], a[i]);
            addEdgesInverse(-b[i], a[i]);
        }
 
        else if (a[i] < 0 && b[i] > 0)
        {
            addEdges(-a[i], b[i]);
            addEdgesInverse(-a[i], b[i]);
            addEdges(b[i] + n, n - a[i]);
            addEdgesInverse(b[i] + n, n - a[i]);
        }
 
        else
        {
            addEdges(-a[i], n - b[i]);
            addEdgesInverse(-a[i], n - b[i]);
            addEdges(-b[i], n - a[i]);
            addEdgesInverse(-b[i], n - a[i]);
        }
    }
 
    // STEP 1 of Kosaraju's Algorithm which
    // traverses the original graph
    for(int i = 1; i <= 2 * n; i++)
        if (!visited[i])
            dfsFirst(i);
 
    // STEP 2 of Kosaraju's Algorithm which
    // traverses the inverse graph. After this,
    // array scc[] stores the corresponding value
    while (!s.isEmpty())
    {
        int top = s.peek();
        s.pop();
 
        if (!visitedInv[top])
        {
            dfsSecond(top);
            counter++;
        }
    }
 
    for(int i = 1; i <= n; i++)
    {
         
        // For any 2 variable x and -x lie in
        // same SCC
        if (scc[i] == scc[i + n])
        {
            System.out.println("The given expression" +
                               "is unsatisfiable.");
            return;
        }
    }
 
    // No such variables x and -x exist which lie
    // in same SCC
    System.out.println("The given expression " +
                       "is satisfiable.");
}
 
// Driver code
public static void main(String[] args)
{
     
    // n is the number of variables
    // 2n is the total number of nodes
    // m is the number of clauses
    int n = 5, m = 7;
 
    for(int i = 0; i < MAX; i++)
    {
        adj.add(new ArrayList());
        adjInv.add(new ArrayList());
    }
 
    // Each clause is of the form a or b
    // for m clauses, we have a[m], b[m]
    // representing a[i] or b[i]
 
    // Note:
    // 1 <= x <= N for an uncomplemented variable x
    // -N <= x <= -1 for a complemented variable x
    // -x is the complement of a variable x
 
    // The CNF being handled is:
    // '+' implies 'OR' and '*' implies 'AND'
    // (x1+x2)*(x2â€™+x3)*(x1â€™+x2â€™)*(x3+x4)*(x3â€™+x5)*
    // (x4â€™+x5â€™)*(x3â€™+x4)
    int a[] = { 1, -2, -1, 3, -3, -4, -3 };
    int b[] = { 2, 3, -2, 4, 5, -5, 4 };
 
    // We have considered the same example
    // for which Implication Graph was made
    is2Satisfiable(n, m, a, b);
}
}
 
// This code is contributed by jithin

输出：

The given expression is satisfiable.

更多测试用例：

Input : n = 2, m = 3
        a[] = {1, 2, -1}
        b[] = {2, -1, -2}
Output : The given expression is satisfiable.

Input : n = 2, m = 4
        a[] = {1, -1, 1, -1}
        b[] = {2, 2, -2, -2}
Output : The given expression is unsatisfiable.