Covering 1.0

#include <bits/stdc++.h>
using namespace std;
unordered_set<int> variables;

void print(vector<int> v) {
    for (int i : v)
        cout << i << " ";
    cout << "\n";
}

void print(vector<vector<int>> v) {
    for (auto i : v)
        print(i);
    cout << "\n";
}

vector<vector<int>> read() {
    string s;
    int l = 1;
    vector<vector<int>> r;
    while (l && getline(cin, s))
        if (s.empty() || s[0] == 'c')
            continue;
        else if (s[0] == 'p') {
            stringstream in;
            in << s;
            int v;
            in >> s >> s >> v >> l;
        } else {
            stringstream in;
            in << s;
            int v;
            vector<int> t;
            while (in >> v && v) {
                t.push_back(v);
                variables.insert(abs(v));
            }
            sort(t.begin(), t.end(), [](int a, int b) {
                return abs(a) < abs(b);
            });
            r.push_back(t);
            l--;
        }
    sort(r.begin(), r.end(), [](vector<int> a, vector<int> b) {
        return a.size() < b.size();
    });
    return r;
}

bool common(vector<int> a, vector<int> b) {
    int i = 0, j = 0;
    while (i < a.size() && j < b.size())
        if (abs(a[i]) == abs(b[j])) {
            if (a[i] != b[j])
                return false;
            i++;
            j++;
        } else if (abs(a[i]) < abs(b[j]))
            i++;
        else j++;
    return true;
}

vector<int> diff(vector<int> a, vector<int> b) {
    unordered_set<int> s;
    for (int i : b)
        s.insert(abs(i));
    vector<int> r;
    for (int i : a)
        if (s.find(abs(i)) == s.end())
            r.push_back(i);
    return r;
}

vector<vector<int>> collide(vector<int> a, vector<int> b) {
    vector<vector<int>> r;
    if (!common(a, b))
        r.push_back(a);
    else {
        vector<int> d = diff(b, a);
//        if (a[0] == 1 && a[1] == -2 && a[2] == -5) {
//            print(b);
//            print(a);
//            cout << "d=";
//            print(d);
//        }
        for (int i : d) {
            vector<int> t = a;
            t.push_back(-i);
            sort(t.begin(), t.end(), [](int a, int b) {
                return abs(a) < abs(b);
            });
            r.push_back(t);
            a.push_back(i);
            //cout << "t=";
            //print(t);
        }
    }
    return r;
}

int main() {
    vector<vector<int>> in = read();
    cout << "#variables=" << variables.size() << "\n";
    cout << "#clauses=" << in.size() << "\n";
//    cout << "clauses:\n";
//    print(in);
//    cout << "\n";
    queue<vector<int>> clauses;
    queue<int> stages;
    for (vector<int> i : in) {
        clauses.push(i);
        stages.push(0);
    }
    vector<vector<int>> cover;
    while (!clauses.empty()) {
        //cout << clauses.size() << " ";
        vector<int> clause = clauses.front();
        //print(clause);
        clauses.pop();
        int stage = stages.front();
        stages.pop();
        if (stage < cover.size()) {
            //cout << "<\n";
            vector<vector<int>> derivatives = collide(clause, cover[stage]);
            for (int i = 0; i < derivatives.size(); i++) {
                clauses.push(derivatives[i]);
                stages.push(stage + 1);
            }
        } else {
            //cout << ">=\n";
            cover.push_back(clause);
            print(cover.back());
//            cout << cover.size() << " ";
        }
    }
    //print(cover);
    vector<int> b(variables.size() + 1);
    for (int i = 0; i < cover.size(); i++)
        b[variables.size() - cover[i].size()]++;
    //print(b);
    bool sat = false;
    for (int i = 0; i < b.size() - 1; i++)
        if (b[i]) {
            if (b[i] % 2)
                sat = true;
            b[i + 1] += b[i] / 2;
        }
    if (b.back() != 1)
        sat = true;
    if (sat)
        cout << "SAT\n";
    else cout << "UNSAT\n";
}