# 算法设计：如何解决2-可满足性（2-SAT）问题？

2021年3月21日17:21:27 发表评论 2,032 次浏览

## 布尔可满足性问题

• 满意的：如果可以为布尔变量分配值, 从而使公式变为TRUE, 则可以说该公式是可满足的。
• 不满意的：如果不可能分配这样的值, 那么我们说该公式是不满足的。

, 是不令人满意的, 因为：

true false false
false true false

## 什么是2-SAT问题

2-SAT是布尔可满足性问题的特例, 可以在多项式时间内求解。

CNF：

CNF是子句的连接(AND), 其中每个子句都是析取(OR)。

``````Input :
Output : The given expression is satisfiable.
(for x1 = FALSE, x2 = TRUE)

Input :
Output : The given expression is unsatisfiable.
(for all possible combinations of x1 and x2)``````

## 2-SAT问题的方法

.

=真

``= TRUE is equivalent to``

• 每个子句2条边, 即" 2m"条边。
• 布尔公式中涉及的每个布尔变量1个节点。

)。

``````CASE 1: If  exists in the graph
This means
If X = TRUE, = TRUE, which is a contradiction.
But if X = FALSE, there are no implication constraints.
Thus, X = FALSE``````
``````CASE 2: If  exists in the graph
This means
If  = TRUE, X = TRUE, which is a contradiction.
But if  = FALSE, there are no implication constraints.
Thus, = FALSE i.e. X = TRUE``````
``````CASE 3: If  both exist in the graph
One edge requires X to be TRUE and the other one requires X to be FALSE.
Thus, there is no possible assignment in such a case.``````

SCC的检查可以在O(E + V)中使用Kosaraju的算法

``````// C++ implementation to find if the given
// expression is satisfiable using the
// Kosaraju's Algorithm
#include <bits/stdc++.h>
using namespace std;

const int MAX = 100000;

// data structures used to implement Kosaraju's
bool visited[MAX];
bool visitedInv[MAX];
stack< int > 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)
{
}

// add edges to form the inverse graph
void addEdgesInverse( int a, int b)
{
}

// for STEP 1 of Kosaraju's Algorithm
void dfsFirst( int u)
{
if (visited[u])
return ;

visited[u] = 1;

s.push(u);
}

// for STEP 2 of Kosaraju's Algorithm
void dfsSecond( int u)
{
if (visitedInv[u])
return ;

visitedInv[u] = 1;

scc[u] = counter;
}

// function to check 2-Satisfiability
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)
{
}

else if (a[i]>0 && b[i]<0)
{
}

else if (a[i]<0 && b[i]>0)
{
}

else
{
}
}

// 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 pf 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 vairable 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
is2Satisfiable(n, m, a, b);

return 0;
}``````

``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.``````