74 lines
1.8 KiB
Java
74 lines
1.8 KiB
Java
|
import java.util.*;
|
||
|
|
import java.util.stream.IntStream;
|
||
|
|
import java.util.stream.Stream;
|
||
|
|
|
||
|
|
// https://en.wikipedia.org/wiki/2-satisfiability
|
||
|
|
public class Sat2 {
|
||
|
|
|
||
|
|
static void dfs1(List<Integer>[] graph, boolean[] used, List<Integer> order, int u) {
|
||
|
|
used[u] = true;
|
||
|
|
for (int v : graph[u])
|
||
|
|
if (!used[v])
|
||
|
|
dfs1(graph, used, order, v);
|
||
|
|
order.add(u);
|
||
|
|
}
|
||
|
|
|
||
|
|
static void dfs2(List<Integer>[] reverseGraph, int[] comp, int u, int color) {
|
||
|
|
comp[u] = color;
|
||
|
|
for (int v : reverseGraph[u])
|
||
|
|
if (comp[v] == -1)
|
||
|
|
dfs2(reverseGraph, comp, v, color);
|
||
|
|
}
|
||
|
|
|
||
|
|
public static boolean[] solve2Sat(List<Integer>[] graph) {
|
||
|
|
int n = graph.length;
|
||
|
|
boolean[] used = new boolean[n];
|
||
|
|
List<Integer> order = new ArrayList<>();
|
||
|
|
for (int i = 0; i < n; ++i)
|
||
|
|
if (!used[i])
|
||
|
|
dfs1(graph, used, order, i);
|
||
|
|
|
||
|
|
List<Integer>[] reverseGraph = Stream.generate(ArrayList::new).limit(n).toArray(List[]::new);
|
||
|
|
for (int i = 0; i < n; i++)
|
||
|
|
for (int j : graph[i])
|
||
|
|
reverseGraph[j].add(i);
|
||
|
|
|
||
|
|
int[] comp = new int[n];
|
||
|
|
Arrays.fill(comp, -1);
|
||
|
|
for (int i = 0, color = 0; i < n; ++i) {
|
||
|
|
int u = order.get(n - i - 1);
|
||
|
|
if (comp[u] == -1)
|
||
|
|
dfs2(reverseGraph, comp, u, color++);
|
||
|
|
}
|
||
|
|
|
||
|
|
for (int i = 0; i < n; ++i)
|
||
|
|
if (comp[i] == comp[i ^ 1])
|
||
|
|
return null;
|
||
|
|
|
||
|
|
boolean[] res = new boolean[n / 2];
|
||
|
|
for (int i = 0; i < n; i += 2)
|
||
|
|
res[i / 2] = comp[i] > comp[i ^ 1];
|
||
|
|
return res;
|
||
|
|
}
|
||
|
|
|
||
|
|
public static void main(String[] args) {
|
||
|
|
int n = 6;
|
||
|
|
List<Integer>[] g = Stream.generate(ArrayList::new).limit(n).toArray(List[]::new);
|
||
|
|
// (a || b) && (b || !c)
|
||
|
|
// !a => b
|
||
|
|
// !b => a
|
||
|
|
// !b => !c
|
||
|
|
// c => b
|
||
|
|
int a = 0, na = 1, b = 2, nb = 3, c = 4, nc = 5;
|
||
|
|
g[na].add(b);
|
||
|
|
g[nb].add(a);
|
||
|
|
g[nb].add(nc);
|
||
|
|
g[c].add(b);
|
||
|
|
|
||
|
|
boolean[] solution = solve2Sat(g);
|
||
|
|
System.out.println(Arrays.toString(solution));
|
||
|
|
|
||
|
|
IntStream.range(0, 10).reduce( (x,y)->x*y).getAsInt();
|
||
|
|
}
|
||
|
|
}
|