C#，布尔可满足性问题（Boolean Satisfiability Problem）算法与源代码
1 布尔可满足性问题
布尔可满足性问题
布尔可满足性或简单的SAT是确定布尔公式是可满足还是不可满足的问题。
可满足：如果布尔变量可以赋值，使得公式为真，那么我们说公式是可满足的。
不可满足：如果无法指定此类值，则我们称公式不可满足。
2 合取范式（CNF）或也称为和积（POS）
为了更好地理解这一点，首先让我们看看什么是合取范式（CNF）或也称为和积（POS）。
CNF：CNF是子句的连词（AND），其中每个子句都是析取（OR）。
现在，2-SAT将SAT问题限制为仅表示为CNF的布尔公式，每个子句只有2个项（也称为2-CNF）。
示例：F=（A\u 1\vee B\u 1）\wedge（A\u 2\vee B\u 2）\wedge（A\u 3\vee B\u 3）\wedge。。。。。。。\楔块（A\u m\vee B\u m）
因此，2-可满足性问题可以表述为：
给定每个子句只有2个项的CNF，是否可以将这些值分配给变量，以使CNF为真？
3 源代码
using System;
using System.IO;
using System.Collections;
using System.Collections.Generic;
namespace Legalsoft.Truffer.Algorithm
{
public static class NP_Complete_Problem
{
private static int MAX { get; set; } = 100000;
private static List<List<int>> adj { get; set; }
private static List<List<int>> adjInv { get; set; }
private static bool[] visited { get; set; } = new bool[MAX];
private static bool[] visitedInv { get; set; } = new bool[MAX];
private static Stack<int> stack { get; set; } = new Stack<int>();
private static int[] scc { get; set; } = new int[MAX];
private static int counter { get; set; } = 1;
public static void Initialize(int n = 5, int m = 7)
{
for (int i = 0; i < MAX; i++)
{
adj.Add(new List<int>());
adjInv.Add(new List<int>());
}
}
private static void Add_Edge(int a, int b)
{
adj[a].Add(b);
}
private static void Add_Edges_Inverse(int a, int b)
{
adjInv[b].Add(a);
}
private static void DFS_First(int u)
{
if (visited[u])
{
return;
}
visited[u] = true;
for (int i = 0; i < adj[u].Count; i++)
{
DFS_First(adj[u][i]);
}
stack.Push(u);
}
private static void DFS_Second(int u)
{
if (visitedInv[u])
{
return;
}
visitedInv[u] = true;
for (int i = 0; i < adjInv[u].Count; i++)
{
DFS_Second(adjInv[u][i]);
}
scc[u] = counter;
}
public static bool Is_2_Satisfiable(int n, int m, int[] a, int[] b)
{
for (int i = 0; i < m; i++)
{
if (a[i] > 0 && b[i] > 0)
{
Add_Edge(a[i] + n, b[i]);
Add_Edges_Inverse(a[i] + n, b[i]);
Add_Edge(b[i] + n, a[i]);
Add_Edges_Inverse(b[i] + n, a[i]);
}
else if (a[i] > 0 && b[i] < 0)
{
Add_Edge(a[i] + n, n - b[i]);
Add_Edges_Inverse(a[i] + n, n - b[i]);
Add_Edge(-b[i], a[i]);
Add_Edges_Inverse(-b[i], a[i]);
}
else if (a[i] < 0 && b[i] > 0)
{
Add_Edge(-a[i], b[i]);
Add_Edges_Inverse(-a[i], b[i]);
Add_Edge(b[i] + n, n - a[i]);
Add_Edges_Inverse(b[i] + n, n - a[i]);
}
else
{
Add_Edge(-a[i], n - b[i]);
Add_Edges_Inverse(-a[i], n - b[i]);
Add_Edge(-b[i], n - a[i]);
Add_Edges_Inverse(-b[i], n - a[i]);
}
}
for (int i = 1; i <= 2 * n; i++)
{
if (!visited[i])
{
DFS_First(i);
}
}
while (stack.Count != 0)
{
int top = stack.Peek();
stack.Pop();
if (!visitedInv[top])
{
DFS_Second(top);
counter++;
}
}
for (int i = 1; i <= n; i++)
{
if (scc[i] == scc[i + n])
{
return false;
}
}
return true;
}
}
}
POWER BY TRUFFER.CN
4 源程序
using System;
using System.IO;
using System.Collections;
using System.Collections.Generic;
namespace Legalsoft.Truffer.Algorithm
{
public static class NP_Complete_Problem
{
private static int MAX { get; set; } = 100000;
private static List<List<int>> adj { get; set; }
private static List<List<int>> adjInv { get; set; }
private static bool[] visited { get; set; } = new bool[MAX];
private static bool[] visitedInv { get; set; } = new bool[MAX];
private static Stack<int> stack { get; set; } = new Stack<int>();
private static int[] scc { get; set; } = new int[MAX];
private static int counter { get; set; } = 1;
public static void Initialize(int n = 5, int m = 7)
{
for (int i = 0; i < MAX; i++)
{
adj.Add(new List<int>());
adjInv.Add(new List<int>());
}
}
private static void Add_Edge(int a, int b)
{
adj[a].Add(b);
}
private static void Add_Edges_Inverse(int a, int b)
{
adjInv[b].Add(a);
}
private static void DFS_First(int u)
{
if (visited[u])
{
return;
}
visited[u] = true;
for (int i = 0; i < adj[u].Count; i++)
{
DFS_First(adj[u][i]);
}
stack.Push(u);
}
private static void DFS_Second(int u)
{
if (visitedInv[u])
{
return;
}
visitedInv[u] = true;
for (int i = 0; i < adjInv[u].Count; i++)
{
DFS_Second(adjInv[u][i]);
}
scc[u] = counter;
}
public static bool Is_2_Satisfiable(int n, int m, int[] a, int[] b)
{
for (int i = 0; i < m; i++)
{
if (a[i] > 0 && b[i] > 0)
{
Add_Edge(a[i] + n, b[i]);
Add_Edges_Inverse(a[i] + n, b[i]);
Add_Edge(b[i] + n, a[i]);
Add_Edges_Inverse(b[i] + n, a[i]);
}
else if (a[i] > 0 && b[i] < 0)
{
Add_Edge(a[i] + n, n - b[i]);
Add_Edges_Inverse(a[i] + n, n - b[i]);
Add_Edge(-b[i], a[i]);
Add_Edges_Inverse(-b[i], a[i]);
}
else if (a[i] < 0 && b[i] > 0)
{
Add_Edge(-a[i], b[i]);
Add_Edges_Inverse(-a[i], b[i]);
Add_Edge(b[i] + n, n - a[i]);
Add_Edges_Inverse(b[i] + n, n - a[i]);
}
else
{
Add_Edge(-a[i], n - b[i]);
Add_Edges_Inverse(-a[i], n - b[i]);
Add_Edge(-b[i], n - a[i]);
Add_Edges_Inverse(-b[i], n - a[i]);
}
}
for (int i = 1; i <= 2 * n; i++)
{
if (!visited[i])
{
DFS_First(i);
}
}
while (stack.Count != 0)
{
int top = stack.Peek();
stack.Pop();
if (!visitedInv[top])
{
DFS_Second(top);
counter++;
}
}
for (int i = 1; i <= n; i++)
{
if (scc[i] == scc[i + n])
{
return false;
}
}
return true;
}
}
}
原文地址：https://blog.csdn.net/beijinghorn/article/details/124891267
免责声明：本站文章内容转载自网络资源，如本站内容侵犯了原著者的合法权益，可联系本站删除。更多内容请关注自学内容网（zxcms.com）！