算法设计(如何解决2-可满足性(2-SAT)问题())

本文概述

  • 布尔可满足性问题
  • 什么是2-SAT问题
  • 建议:在继续解决方案之前, 请先在{IDE}上尝试使用你的方法。
  • 2-SAT问题的方法
布尔可满足性问题 布尔可满足性或简单SAT考试是确定布尔公式是否可满足或无法满足的问题。
  • 满意的:如果可以为布尔变量分配值, 从而使公式变为TRUE, 则可以说该公式是可满足的。
  • 不满意的:如果不可能分配这样的值, 那么我们说该公式是不满足的。
例子:
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
可以满足, 因为A = TRUE和B = FALSE使F = TRUE。
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
, 是不令人满意的, 因为:
true false false
false true false
注:布尔可满足性问题是np完全的(关于证明,参考库克定理 https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem)。
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
什么是2-SAT问题
2-SAT是布尔可满足性问题的特例, 可以在多项式时间内求解。
【算法设计(如何解决2-可满足性(2-SAT)问题())】为了更好地理解这一点, 首先让我们看看什么是合取范式(CNF)或也称为和积(POS)。
CNF:
CNF是子句的连接(AND), 其中每个子句都是析取(OR)。
现在, 2-SAT将SAT问题限制为仅将那些布尔表达式表示为CNF, 而每个子句仅具有2学期(也被称为2-CNF)。
例子:
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
因此, 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。让条款之一
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
.
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
=真
如果A = 0, 则B必须为1, 即
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
如果B = 0, 则A必须为1, 即
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
从而,
= TRUE is equivalent to

现在, 我们可以将CNF表示为蕴涵。因此, 我们为CNF的每个子句创建一个具有2条边的隐含图。
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
在隐含图中表示为
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
因此, 对于带有" m"子句的布尔公式, 我们制作一个具有以下含义的隐含图:
  • 每个子句2条边, 即" 2m"条边。
  • 布尔公式中涉及的每个布尔变量1个节点。
让我们看一个蕴涵图的例子。
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
注意:
含义(如果从A到B, 则等价)等于其对立的(如果从
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
然后
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
)。
现在, 考虑以下情况:
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.

结论:
如果有两个变量
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片

算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
处于周期中
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
两者都存在, 那么CNF是无法满足的。否则, 可能存在分配并且CNF是可满足的。
请注意, 由于以下含义, 我们使用路径:
如果我们有
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
因此, 如果我们在隐含图中有一条路径, 则与具有直接边几乎相同。
从实施观点出发的结论:
如果X和
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
如果在同一SCC(牢固连接的组件)中, 则CNF不能令人满意。
有向图的强连接组件具有节点, 因此可以从该SCC中的每个其他节点访问每个节点。
现在, 如果X和
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
躺在同一SCC上, 我们肯定会
算法设计(如何解决2-可满足性(2-SAT)问题())

文章图片
现在, 因此得出结论。
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.

如果发现任何不正确的地方, 或者想分享有关上述主题的更多信息, 请写评论。

    推荐阅读