-
Notifications
You must be signed in to change notification settings - Fork 23
Expand file tree
/
Copy path2sat.cpp
More file actions
144 lines (133 loc) · 3.63 KB
/
2sat.cpp
File metadata and controls
144 lines (133 loc) · 3.63 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
#define SCCNODE adf
struct SCC{
int num[SCCNODE], low[SCCNODE], col[SCCNODE], cycle[SCCNODE], st[SCCNODE];
int tail, cnt, cc;
vi adj[SCCNODE];
SCC():tail(0),cnt(0),cc(0) {}
void clear ( int n ) {
cc += 3;
FOR(i,0,n) adj[i].clear();
tail = 0;
}
void tarjan ( int s ) {
num[s] = low[s] = cnt++;
col[s] = cc + 1;
st[tail++] = s;
FOR(i,0,SZ(adj[s])-1) {
int t = adj[s][i];
if ( col[t] <= cc ) {
tarjan ( t );
low[s]=min(low[s],low[t]);
}
/*Back edge*/
else if (col[t]==cc+1)
low[s]=min(low[s],low[t]);
}
if ( low[s] == num[s] ) {
while ( 1 ) {
int temp=st[tail-1];
tail--;
col[temp] = cc + 2;
cycle[temp] = s;
if ( s == temp ) break;
}
}
}
void shrink( int n ) {
FOR(i,0,n){
FOR(j,0,SZ(adj[i])-1){
adj[i][j] = cycle[adj[i][j]]; ///Careful. This will create self-loop
}
}
FOR(i,0,n){
if ( cycle[i] == i ) continue;
int u = cycle[i];
FOR(j,0,SZ(adj[i])-1){
int v = adj[i][j];
adj[u].pb ( v );
}
adj[i].clear();
}
FOR(i,0,n){ ///Not always necessary
sort ( ALL(adj[i]) );
UNIQUE(adj[i]);
}
}
void findSCC( int n ) {
FOR(i,0,n) {
if ( col[i] <= cc ) {
tarjan ( i );
}
}
}
};
/*
1. The nodes need to be split. So change convert() accordingly.
2. Using clauses, populate scc edges.
3. Call possible, to find if a valid solution is possible or not.
4. Dont forget to keep space for !A variables
*/
struct SAT2 {
SCC scc;
SAT2(): bfscc(1) {}
void clear( int n ) {
scc.clear( int n );
}
int convert ( int n ) { ///Change here. Depends on how input is provided
int x = ABS(n);
x--;
x *= 2;
if ( n < 0 ) x ^= 1;
return x;
}
void mustTrue ( int a ) { ///A is True
scc.adj[a^1].pb ( a );
}
void orClause ( int a, int b ) { /// A || B clause
//!a->b !b->a
scc.adj[a^1].pb ( b );
scc.adj[b^1].pb ( a );
}
/// Out of all possible option, only one is true
void atMostOneClause ( int a[], int n, int flag ) {
if ( flag == 0 ) { /// At most one can be false
FOR(i,0,n){
a[i] = a[i] ^ 1;
}
}
FOR(i,0,n) {
FOR(j,i+1,n) {
orClause( a[i] ^ 1, a[j] ^ 1 ); /// !a || !b both being true not allowed
}
}
}
///Send n, total number of nodes, after expansion
bool possible( int n ) {
scc.findSCC( n );
FOR(i,0,n) {
int a = i, b = i^1;
///Falls on same cycle a and !a.
if ( scc.cycle[a] == scc.cycle[b] ) return false;
}
///Valid solution exists
return true;
}
///To determine if A can be true. It cannot be true, if a path exists from A to !A.
int vis[SAT2NODE], qqq[SAT2NODE], bfscc;
void bfs( int s ) {
bfscc++;
int qs = 0, qt = 0;
vis[s] = bfscc;
qqq[qt++] = s;
while ( qs < qt ) {
s = qqq[qs++];
FOR(i,0,SZ(scc.adj[s])-1) {
int t = scc.adj[s][i];
if ( vis[t] != bfscc ) {
vis[t] = bfscc;
qqq[qt++] = t;
}
}
}
}
}sat2;