wangzirui

Covering 1.0

Aug 20th, 2019
21
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #include <bits/stdc++.h>
  2. using namespace std;
  3. unordered_set<int> variables;
  4.  
  5. void print(vector<int> v) {
  6.     for (int i : v)
  7.         cout << i << " ";
  8.     cout << "\n";
  9. }
  10.  
  11. void print(vector<vector<int>> v) {
  12.     for (auto i : v)
  13.         print(i);
  14.     cout << "\n";
  15. }
  16.  
  17. vector<vector<int>> read() {
  18.     string s;
  19.     int l = 1;
  20.     vector<vector<int>> r;
  21.     while (l && getline(cin, s))
  22.         if (s.empty() || s[0] == 'c')
  23.             continue;
  24.         else if (s[0] == 'p') {
  25.             stringstream in;
  26.             in << s;
  27.             int v;
  28.             in >> s >> s >> v >> l;
  29.         } else {
  30.             stringstream in;
  31.             in << s;
  32.             int v;
  33.             vector<int> t;
  34.             while (in >> v && v) {
  35.                 t.push_back(v);
  36.                 variables.insert(abs(v));
  37.             }
  38.             sort(t.begin(), t.end(), [](int a, int b) {
  39.                 return abs(a) < abs(b);
  40.             });
  41.             r.push_back(t);
  42.             l--;
  43.         }
  44.     sort(r.begin(), r.end(), [](vector<int> a, vector<int> b) {
  45.         return a.size() < b.size();
  46.     });
  47.     return r;
  48. }
  49.  
  50. bool common(vector<int> a, vector<int> b) {
  51.     int i = 0, j = 0;
  52.     while (i < a.size() && j < b.size())
  53.         if (abs(a[i]) == abs(b[j])) {
  54.             if (a[i] != b[j])
  55.                 return false;
  56.             i++;
  57.             j++;
  58.         } else if (abs(a[i]) < abs(b[j]))
  59.             i++;
  60.         else j++;
  61.     return true;
  62. }
  63.  
  64. vector<int> diff(vector<int> a, vector<int> b) {
  65.     unordered_set<int> s;
  66.     for (int i : b)
  67.         s.insert(abs(i));
  68.     vector<int> r;
  69.     for (int i : a)
  70.         if (s.find(abs(i)) == s.end())
  71.             r.push_back(i);
  72.     return r;
  73. }
  74.  
  75. vector<vector<int>> collide(vector<int> a, vector<int> b) {
  76.     vector<vector<int>> r;
  77.     if (!common(a, b))
  78.         r.push_back(a);
  79.     else {
  80.         vector<int> d = diff(b, a);
  81. //        if (a[0] == 1 && a[1] == -2 && a[2] == -5) {
  82. //            print(b);
  83. //            print(a);
  84. //            cout << "d=";
  85. //            print(d);
  86. //        }
  87.         for (int i : d) {
  88.             vector<int> t = a;
  89.             t.push_back(-i);
  90.             sort(t.begin(), t.end(), [](int a, int b) {
  91.                 return abs(a) < abs(b);
  92.             });
  93.             r.push_back(t);
  94.             a.push_back(i);
  95.             //cout << "t=";
  96.             //print(t);
  97.         }
  98.     }
  99.     return r;
  100. }
  101.  
  102. int main() {
  103.     vector<vector<int>> in = read();
  104.     cout << "#variables=" << variables.size() << "\n";
  105.     cout << "#clauses=" << in.size() << "\n";
  106. //    cout << "clauses:\n";
  107. //    print(in);
  108. //    cout << "\n";
  109.     queue<vector<int>> clauses;
  110.     queue<int> stages;
  111.     for (vector<int> i : in) {
  112.         clauses.push(i);
  113.         stages.push(0);
  114.     }
  115.     vector<vector<int>> cover;
  116.     while (!clauses.empty()) {
  117.         //cout << clauses.size() << " ";
  118.         vector<int> clause = clauses.front();
  119.         //print(clause);
  120.         clauses.pop();
  121.         int stage = stages.front();
  122.         stages.pop();
  123.         if (stage < cover.size()) {
  124.             //cout << "<\n";
  125.             vector<vector<int>> derivatives = collide(clause, cover[stage]);
  126.             for (int i = 0; i < derivatives.size(); i++) {
  127.                 clauses.push(derivatives[i]);
  128.                 stages.push(stage + 1);
  129.             }
  130.         } else {
  131.             //cout << ">=\n";
  132.             cover.push_back(clause);
  133.             print(cover.back());
  134. //            cout << cover.size() << " ";
  135.         }
  136.     }
  137.     //print(cover);
  138.     vector<int> b(variables.size() + 1);
  139.     for (int i = 0; i < cover.size(); i++)
  140.         b[variables.size() - cover[i].size()]++;
  141.     //print(b);
  142.     bool sat = false;
  143.     for (int i = 0; i < b.size() - 1; i++)
  144.         if (b[i]) {
  145.             if (b[i] % 2)
  146.                 sat = true;
  147.             b[i + 1] += b[i] / 2;
  148.         }
  149.     if (b.back() != 1)
  150.         sat = true;
  151.     if (sat)
  152.         cout << "SAT\n";
  153.     else cout << "UNSAT\n";
  154. }
RAW Paste Data

Adblocker detected! Please consider disabling it...

We've detected AdBlock Plus or some other adblocking software preventing Pastebin.com from fully loading.

We don't have any obnoxious sound, or popup ads, we actively block these annoying types of ads!

Please add Pastebin.com to your ad blocker whitelist or disable your adblocking software.

×