本文概述
- 布尔可满足性问题
- 什么是2-SAT问题
- 建议:在继续解决方案之前, 请先在{IDE}上尝试使用你的方法。
- 2-SAT问题的方法
- 满意的:如果可以为布尔变量分配值, 从而使公式变为TRUE, 则可以说该公式是可满足的。
- 不满意的:如果不可能分配这样的值, 那么我们说该公式是不满足的。
文章图片
可以满足, 因为A = TRUE和B = FALSE使F = TRUE。
文章图片
, 是不令人满意的, 因为:
true | false | false |
false | true | false |
文章图片
什么是2-SAT问题
2-SAT是布尔可满足性问题的特例, 可以在多项式时间内求解。【算法设计(如何解决2-可满足性(2-SAT)问题())】为了更好地理解这一点, 首先让我们看看什么是合取范式(CNF)或也称为和积(POS)。
CNF:
CNF是子句的连接(AND), 其中每个子句都是析取(OR)。
现在, 2-SAT将SAT问题限制为仅将那些布尔表达式表示为CNF, 而每个子句仅具有2学期(也被称为2-CNF)。
例子:
文章图片
因此, 2满足性问题可以表述为:
给定CNF, 每个子句只有2个项, 是否可以将这些值分配给变量, 以使CNF为TRUE?
例子:
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)
推荐:请尝试以下方法{IDE}首先, 在继续解决方案之前。 2-SAT问题的方法 为了使CNF值变为TRUE, 每个子句的值都应为TRUE。让条款之一
文章图片
.
文章图片
=真
如果A = 0, 则B必须为1, 即
文章图片
如果B = 0, 则A必须为1, 即
文章图片
从而,
= TRUE is equivalent to
现在, 我们可以将CNF表示为蕴涵。因此, 我们为CNF的每个子句创建一个具有2条边的隐含图。
文章图片
在隐含图中表示为
文章图片
因此, 对于带有" m"子句的布尔公式, 我们制作一个具有以下含义的隐含图:
- 每个子句2条边, 即" 2m"条边。
- 布尔公式中涉及的每个布尔变量1个节点。
文章图片
文章图片
注意:
含义(如果从A到B, 则等价)等于其对立的(如果从
文章图片
然后
文章图片
)。
现在, 考虑以下情况:
CASE 1: Ifexists 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: Ifexists 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: Ifboth 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.
结论:
如果有两个变量
文章图片
和
文章图片
处于周期中
文章图片
两者都存在, 那么CNF是无法满足的。否则, 可能存在分配并且CNF是可满足的。
请注意, 由于以下含义, 我们使用路径:
如果我们有
文章图片
因此, 如果我们在隐含图中有一条路径, 则与具有直接边几乎相同。
从实施观点出发的结论:
如果X和
文章图片
如果在同一SCC(牢固连接的组件)中, 则CNF不能令人满意。
有向图的强连接组件具有节点, 因此可以从该SCC中的每个其他节点访问每个节点。
现在, 如果X和
文章图片
躺在同一SCC上, 我们肯定会
文章图片
现在, 因此得出结论。
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
// Algorithm. Please refer
vector<
int >
adj[MAX];
vector<
int >
adjInv[MAX];
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)
{
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<
adj[u].size();
i++)
dfsFirst(adj[u][i]);
s.push(u);
}// for STEP 2 of Kosaraju's Algorithm
void dfsSecond( int u)
{
if (visitedInv[u])
return ;
visitedInv[u] = 1;
for ( int i=0;
i<
adjInv[u].size();
i++)
dfsSecond(adjInv[u][i]);
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)
{
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 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
// Implication Graph was made
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.
如果发现任何不正确的地方, 或者想分享有关上述主题的更多信息, 请写评论。
推荐阅读
- 如何实现图像2D转换(|物体旋转)
- 计算机图形学中的2D转换算法实现|S1(对象缩放)
- 2D和2.5D内存组织是什么(有什么区别?)
- 算法题(如何实现1和2的二进制补码())
- 计算将N表示为1,3和4的和的方法|算法题
- 算法题(如何连接树中相同层级的节点())
- 算法题(如何实现求和树())
- 如何解决0-1背包问题(| DP-10(动态规划))
- C/C++棘手程序集锦和详细介绍