C#，布尔可满足性问题（Boolean Satisfiability Problem）算法与源代码

本文主要是介绍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]);
}
}