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
|
#include "../util.h"
#include <graph/scc.cpp>
#include <graph/2sat.cpp>
struct RandomClause {
int a, b;
int type;
RandomClause(int n) :
a(Random::integer<int>(0, 2*n)),
b(Random::integer<int>(0, 2*n)),
type(Random::integer<int>(0, 8)) {}
bool eval(vector<int>& sol) const {
bool ba = sol[a];
bool bb = sol[b];
if (type == 0) return !ba || bb;
if (type == 1) return ba == bb;
if (type == 2) return ba || bb;
if (type == 3) return ba != bb;
if (type == 4) return ba && bb;
if (type == 5) return !(ba && bb);
if (type == 6) return ba;
if (type == 7) return !ba;
return false;
}
void add(SAT2& sat) const {
int va = a;
int vb = b;
if (type == 0) sat.addImpl(va, vb);
if (type == 1) sat.addEquiv(va, vb);
if (type == 2) sat.addOr(va, vb);
if (type == 3) sat.addXor(va, vb);
if (type == 4) sat.addAnd(va, vb);
if (type == 5) sat.addNand(va, vb);
if (type == 6) sat.addTrue(va);
if (type == 7) sat.addFalse(va);
}
friend ostream& operator<<(ostream& os, const RandomClause& c) {
if (c.a & 1) os << "-";
os << (c.a >> 1);
if (c.type == 0) os << "=>";
if (c.type == 1) os << "==";
if (c.type == 2) os << "or";
if (c.type == 3) os << "xor";
if (c.type == 4) os << "and";
if (c.type == 5) os << "nand";
if (c.type == 6) return os;
if (c.type == 7) return os << "==F";
if (c.b & 1) os << "-";
os << (c.b >> 1);
return os;
}
};
bool naive(int n, const vector<RandomClause>& clauses) {
for (ll i = 0; i < (1ll << n); i++) {
vector<int> tmp(2*n);
for (ll j = 0; j < n; j++) {
tmp[(2*j) + ((i >> j) & 1)] = 1;
}
bool ok = true;
for (auto& c : clauses) ok &= c.eval(tmp);
if (ok) return true;
}
return false;
}
void stress_test() {
ll queries = 0;
for (int tries = 0; tries < 200'000; tries++) {
int n = Random::integer<int>(1, 12);
int m = Random::integer<int>(0, 30);
vector<RandomClause> clauses;
for (int i = 0; i < m; i++) clauses.emplace_back(n);
SAT2 sat(n);
for (auto& c : clauses) c.add(sat);
bool got = sat.solve();
bool expected = naive(n, clauses);
if (got) {
for (int i = 0; i < 2*n; i+=2) {
if (sat.sol[i] < 0) cerr << "error: invalid vars" << FAIL;
if (sat.sol[i+1] < 0) cerr << "error: invalid vars" << FAIL;
if (sat.sol[i] == sat.sol[i+1]) cerr << "error: inconsistent vars" << FAIL;
}
for (auto& c : clauses) {
if (!c.eval(sat.sol)) {
cerr << "error: inconsistent" << FAIL;
}
}
}
if (got != expected) cerr << "got: " << got << ", expected: " << expected << FAIL;
queries += n;
}
cerr << "tested random queries: " << queries << endl;
}
constexpr int N = 200'000;
constexpr int M = 500'000;
void performance_test() {
timer t;
vector<RandomClause> clauses;
for (int i = 0; i < M; i++) clauses.emplace_back(N);
t.start();
SAT2 sat(N);
for (auto& c : clauses) c.add(sat);
hash_t hash = sat.solve();
t.stop();
if (t.time > 500) cerr << "too slow: " << t.time << FAIL;
cerr << "tested performance: " << t.time << "ms (hash: " << hash << ")" << endl;
}
int main() {
stress_test();
performance_test();
}
|
