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
|
#include <bits/stdc++.h>
using namespace std;
struct Edge {
int from;
int to;
};
struct ConvertHampathToSat {
int numVertices;
vector<Edge> edges;
ConvertHampathToSat(int n, int m) :
numVertices(n),
edges(m)
{ }
// matrix of vertices * vertices (+1 because 0 is reserved)
static inline int var(int v1, int v2, int n) { return 1 + v1 * n + v2; }
void printEquisatisfiableSatFormula() {
vector<vector<int>> clauses;
vector<int> cstrs;
for (int i = 0; i < numVertices; i++) {
// the vertex belongs to the path, matrix rows
cstrs.clear();
for (int j = 0; j < numVertices; j++)
cstrs.push_back(var(i, j, numVertices)); // (Xi0 || Xi1 || Xi2 ...)
clauses.push_back(cstrs);
// the vertex appears just once in the path
for (int j = 0; j < numVertices; j++) {
for (int k = j + 1; k < numVertices; k++)
clauses.push_back({-var(i, j, numVertices), -var(i, k, numVertices)}); // ( !Xij && !Xik )
}
// each position in the path has a vertex, matrix cols
cstrs.clear();
for (int j = 0; j < numVertices; j++)
cstrs.push_back(var(j, i, numVertices)); // (X0i || X1i || X2i ...)
clauses.push_back(cstrs);
// each position has only 1 vertex
for (int j = 0; j < numVertices; j++) {
for (int k = j + 1; k < numVertices; k++)
clauses.push_back({-var(j, i, numVertices), -var(k, i, numVertices)}); // ( !Xji && !Xki )
}
// if there is no ij edje, there is no Xik Xj(k+1) or Xjk Xi(k+1)
for (int j = i + 1; j < numVertices; j++) {
// would be much faster with an adjacent matrix
bool found = false;
for (Edge e : edges) {
if ((e.from == i+1 && e.to == j+1) || (e.from == j+1 && e.to == i+1)) {
found = true;
break;
}
}
if (!found) {
// no v-w edge
for (int k = 0; k < (numVertices - 1); k++) {
clauses.push_back({-var(i, k, numVertices), -var(j, k + 1, numVertices)}); // ( !Xik && !Xj(k+1)
clauses.push_back({-var(j, k, numVertices), -var(i, k + 1, numVertices)}); // ( !Xjk && !Xi(k+1)
}
}
}
}
cout << clauses.size() << " " << numVertices * numVertices << endl;
for (vector<int>& c : clauses) {
for (int v : c) {
cout << v << " ";
}
cout << "0" << endl;
}
cout << endl;
}
};
int main() {
ios::sync_with_stdio(false);
int n, m;
cin >> n >> m;
ConvertHampathToSat converter(n, m);
for (int i = 0; i < m; ++i) {
cin >> converter.edges[i].from >> converter.edges[i].to;
}
converter.printEquisatisfiableSatFormula();
return 0;
}
|
