diff options
| author | Gloria Mundi <gloria@gloria-mundi.eu> | 2024-11-16 01:24:14 +0100 |
|---|---|---|
| committer | Gloria Mundi <gloria@gloria-mundi.eu> | 2024-11-16 01:24:14 +0100 |
| commit | 98567ec798aa8ca2cfbcb85c774dd470f30e30d4 (patch) | |
| tree | 5113d5cc24d1ad5f93810b6442ce584a36950dc8 /content/graph/2sat.cpp | |
| parent | ad3856a6b766087df0036de0b556f4700a6498c9 (diff) | |
| parent | 8d11c6c8213f46f0fa19826917c255edd5d43cb1 (diff) | |
mzuenni tests
Diffstat (limited to 'content/graph/2sat.cpp')
| -rw-r--r-- | content/graph/2sat.cpp | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/content/graph/2sat.cpp b/content/graph/2sat.cpp new file mode 100644 index 0000000..75e54e6 --- /dev/null +++ b/content/graph/2sat.cpp @@ -0,0 +1,31 @@ +struct sat2 { + int n; // + scc variablen + vector<int> sol; + + sat2(int vars) : n(vars*2), adj(n) {} + + static int var(int i) {return i << 1;} // use this! + + void addImpl(int a, int b) { + adj[a].push_back(b); + adj[1^b].push_back(1^a); + } + void addEquiv(int a, int b) {addImpl(a, b); addImpl(b, a);} + void addOr(int a, int b) {addImpl(1^a, b);} + void addXor(int a, int b) {addOr(a, b); addOr(1^a, 1^b);} + void addTrue(int a) {addImpl(1^a, a);} + void addFalse(int a) {addTrue(1^a);} + void addAnd(int a, int b) {addTrue(a); addTrue(b);} + void addNand(int a, int b) {addOr(1^a, 1^b);} + + bool solve() { + scc(); //scc code von oben + sol.assign(n, -1); + for (int i = 0; i < n; i += 2) { + if (idx[i] == idx[i + 1]) return false; + sol[i] = idx[i] < idx[i + 1]; + sol[i + 1] = !sol[i]; + } + return true; + } +}; |
