// m12pc.cpp -- Kernextraktion (DPLL + Streich-MUS) und PC-Grad ueber GF(2) fuer M12.
// Bauen:  g++ -O3 -march=native -o m12pc m12pc.cpp
// Aufruf: m12pc mus            stdin: "n m" + m Klauseln (Literale, 0-terminiert)  -> "SAT" | "UNSAT j1 j2 ..."
//         m12pc pc dmin dmax tmax memgb [voll]   stdin: "k m" + Klauseln (Variablen 1..k)
//                                   -> "grad gek rang sekunden speicherMB vneu runden"   gek: 0 fertig, 1 Zeit, 2 Speicher
//                                      rang: Basisgroesse beim letzten Grad (auch beim Fixpunkt ohne 1)
//                                      vneu: Basiszeilen, die nur die volle Regel geliefert hat; runden: Phase-B-Durchlaeufe
// MUS: Streichverfahren in Index-Reihenfolge, identisch zu m9_kern.mus (nur ohne 2^n-Tabelle).
// PC:  multilinear (x^2=x), Multiplikation x*p nur fuer Grad(p) < d; Monom-Reihenfolge wie m8_nsgrad.monom_index.
// voll=1 (M12b): volle Regel -- x*p auch fuer Grad(p) = d, wenn x in jedem Grad-d-Monom von p vorkommt (dann bleibt
//       der Grad nach x^2=x bei d). Exakt ueber den ganzen Spann: fuer jedes x wird der Teilraum
//       V_x = { p im Spann : alle Grad-d-Monome von p enthalten x } per Elimination auf den "schlechten" Spalten
//       (Grad-d-Monome ohne x) bestimmt; x*V_x wird eingefuegt; Wechsel mit dem FIFO-Abschluss bis zum Fixpunkt.
#include <bits/stdc++.h>
using namespace std;
typedef uint64_t u64;
static double now() { return chrono::duration<double>(chrono::steady_clock::now().time_since_epoch()).count(); }

static vector<vector<int>> readcnf(int& n) {
    int m; cin >> n >> m; vector<vector<int>> C(m);
    for (int j = 0; j < m; j++) { int l; while (cin >> l && l != 0) C[j].push_back(l); }
    return C;
}

// ---------------- DPLL ----------------
struct Solver {
    int n; const vector<vector<int>>& C; vector<char> act; vector<vector<int>> occ; vector<int> val, trail;
    Solver(int n, const vector<vector<int>>& C) : n(n), C(C), act(C.size(), 1), occ(2 * n + 2), val(n + 1, 0) {
        for (int j = 0; j < (int)C.size(); j++) for (int l : C[j]) occ[li(l)].push_back(j);
    }
    static int li(int l) { return l > 0 ? 2 * l : 2 * (-l) + 1; }
    int lv(int l) const { int v = val[abs(l)]; return l > 0 ? v : -v; }
    bool assign(int l) {
        vector<int> q{l};
        while (!q.empty()) {
            int x = q.back(); q.pop_back(); int s = lv(x);
            if (s == 1) continue; if (s == -1) return false;
            val[abs(x)] = x > 0 ? 1 : -1; trail.push_back(abs(x));
            for (int j : occ[li(-x)]) {
                if (!act[j]) continue; int un = 0, ul = 0; bool sat = false;
                for (int y : C[j]) { int t = lv(y); if (t == 1) { sat = true; break; } if (t == 0) { un++; ul = y; } }
                if (sat) continue; if (un == 0) return false; if (un == 1) q.push_back(ul);
            }
        }
        return true;
    }
    void undo(size_t mark) { while (trail.size() > mark) { val[trail.back()] = 0; trail.pop_back(); } }
    bool solve() {                                   // true = erfuellbar
        int best = 0, bl = 99;
        for (size_t j = 0; j < C.size(); j++) {
            if (!act[j]) continue; int un = 0, ul = 0; bool sat = false;
            for (int y : C[j]) { int t = lv(y); if (t == 1) { sat = true; break; } if (t == 0) { un++; ul = y; } }
            if (sat) continue; if (un == 0) return false; if (un < bl) { bl = un; best = ul; }
        }
        if (best == 0) return true;
        size_t mark = trail.size();
        if (assign(best) && solve()) return true; undo(mark);
        if (assign(-best) && solve()) return true; undo(mark);
        return false;
    }
    bool sat() { trail.clear(); fill(val.begin(), val.end(), 0); return solve(); }
};

static int cmd_mus() {
    int n; auto C = readcnf(n); Solver S(n, C);
    if (S.sat()) { puts("SAT"); return 0; }
    for (size_t j = 0; j < C.size(); j++) { S.act[j] = 0; if (S.sat()) S.act[j] = 1; }
    printf("UNSAT"); for (size_t j = 0; j < C.size(); j++) if (S.act[j]) printf(" %zu", j); puts("");
    return 0;
}

// ---------------- PC ueber GF(2) ----------------
struct PC {
    int k, d, N = 0, lowmax = 0, W = 0;
    unordered_map<u64, int> idx; vector<int> mul; vector<u64> mons; int voll = 0; long runden = 0, vneu = 0;
    vector<vector<u64>> rows; vector<int> top, piv, queue; vector<u64> r; size_t bytes = 0, memcap = 0;
    PC(int k, int d) : k(k), d(d) {
        for (int dd = 0; dd <= d && dd <= k; dd++) {
            vector<int> c(dd); for (int i = 0; i < dd; i++) c[i] = i;
            while (true) {
                u64 m = 0; for (int v : c) m |= 1ULL << v;
                idx[m] = mons.size(); mons.push_back(m);
                int i = dd - 1; while (i >= 0 && c[i] == k - dd + i) i--;
                if (i < 0) break; c[i]++; for (int j = i + 1; j < dd; j++) c[j] = c[j - 1] + 1;
            }
            if (dd == d - 1) lowmax = mons.size();
        }
        N = mons.size(); W = (N + 63) / 64; r.assign(W, 0); piv.assign(N, -1);
        mul.assign((size_t)lowmax * k, 0);
        for (int i = 0; i < lowmax; i++) for (int v = 0; v < k; v++) mul[(size_t)i * k + v] = idx.at(mons[i] | (1ULL << v));
    }
    inline void flip(int ix) { r[ix >> 6] ^= 1ULL << (ix & 63); }
    // reduziert r gegen die Basis; speichert den Rest. Danach ist r wieder 0. -> 1 wenn Konstante 1 gefunden.
    int insert() {
        int t = W - 1;
        while (true) {
            while (t >= 0 && r[t] == 0) t--;
            if (t < 0) return 0;
            int p = t * 64 + 63 - __builtin_clzll(r[t]); int q = piv[p];
            if (q < 0) {
                piv[p] = rows.size(); rows.emplace_back(r.begin(), r.begin() + t + 1); top.push_back(t);
                bytes += 8 * (size_t)(t + 1) + 32;
                if (p < lowmax) queue.push_back(rows.size() - 1);
                fill(r.begin(), r.begin() + t + 1, 0);
                return p == 0;
            }
            const u64* a = rows[q].data(); u64* b = r.data(); int tq = top[q];
            for (int w = 0; w <= tq; w++) b[w] ^= a[w];
        }
    }
    int run(const vector<vector<int>>& C, double t0, double tmax) {   // 1 widerlegt, 0 Fixpunkt, -1 Zeit, -2 Speicher
        for (auto& c : C) {
            u64 neg = 0; vector<int> pos;
            for (int l : c) { if (l > 0) pos.push_back(l - 1); else neg |= 1ULL << (-l - 1); }
            for (int s = 0; s < (1 << pos.size()); s++) {
                u64 m = neg; for (size_t i = 0; i < pos.size(); i++) if (s >> i & 1) m |= 1ULL << pos[i];
                flip(idx.at(m));
            }
            if (insert()) return 1;
        }
        vector<int> bits; long cnt = 0;
        size_t qh = 0;
        while (true) {
            while (qh < queue.size()) {                                   // Phase A: x*p fuer Grad(p) < d (FIFO)
                int qi = queue[qh++]; bits.clear();
                const auto& R = rows[qi];
                for (size_t w = 0; w < R.size(); w++) { u64 x = R[w]; while (x) { bits.push_back(w * 64 + __builtin_ctzll(x)); x &= x - 1; } }
                for (int v = 0; v < k; v++) {
                    for (int b : bits) flip(mul[(size_t)b * k + v]);
                    if (insert()) return 1;
                    if (bytes > memcap) return -2;
                }
                if ((++cnt & 7) == 0 && now() - t0 > tmax) return -1;
            }
            if (!voll) return 0;
            int res = phaseB(t0, tmax);                                   // Phase B: volle Regel fuer Grad(p) = d
            if (res != 2) return res;                                     // 2 = etwas Neues -> Phase A erneut
        }
    }
    // -> 1 widerlegt, 0 nichts Neues (Fixpunkt), 2 neue Zeilen, -1 Zeit, -2 Speicher
    int phaseB(double t0, double tmax) {
        runden++;
        size_t before = rows.size();
        vector<int> topr;                                                 // Basiszeilen mit Grad-d-Pivot
        for (int p = lowmax; p < N; p++) if (piv[p] >= 0) topr.push_back(piv[p]);
        if (topr.empty()) return 0;
        int w0 = lowmax >> 6;                                             // erstes Wort mit Grad-d-Spalten
        vector<u64> bad(W);
        vector<int> tpiv(N, -1); vector<vector<u64>> T; vector<int> ttop; vector<u64> t(W), xp(W);
        for (int x = 0; x < k; x++) {
            u64 xb = 1ULL << x;
            fill(bad.begin(), bad.end(), 0);
            for (int i = lowmax; i < N; i++) if (!(mons[i] & xb)) bad[i >> 6] |= 1ULL << (i & 63);
            T.clear(); ttop.clear(); size_t tbytes = 0;
            fill(tpiv.begin(), tpiv.end(), -1);
            vector<vector<u64>> kern;
            for (int ri : topr) {
                fill(t.begin(), t.end(), 0);
                const auto& R = rows[ri]; for (size_t w = 0; w < R.size(); w++) t[w] = R[w];
                int tt = (int)R.size() - 1;
                while (true) {
                    int w = tt; while (w >= w0 && !(t[w] & bad[w])) w--;
                    if (w < w0) { kern.emplace_back(t.begin(), t.begin() + tt + 1); tbytes += 8 * (size_t)(tt + 1); break; }
                    int p = w * 64 + 63 - __builtin_clzll(t[w] & bad[w]); int q = tpiv[p];
                    if (q < 0) { tpiv[p] = T.size(); T.emplace_back(t.begin(), t.begin() + tt + 1); ttop.push_back(tt); tbytes += 8 * (size_t)(tt + 1) + 32; break; }
                    const u64* a = T[q].data(); int tq = ttop[q]; for (int u = 0; u <= tq; u++) t[u] ^= a[u];
                    if (tq > tt) tt = tq;
                }
                if (bytes + tbytes > memcap) return -2;
            }
            T.clear();
            for (auto& v : kern) {                                       // x*v einfuegen
                for (size_t w = 0; w < v.size(); w++) { u64 z = v[w]; while (z) { int b = w * 64 + __builtin_ctzll(z); z &= z - 1;
                    if (b < lowmax) flip(mul[(size_t)b * k + x]); else flip(b); } }
                size_t rb = rows.size();
                if (insert()) return 1;
                if (rows.size() > rb) vneu++;
                if (bytes > memcap) return -2;
            }
            if (now() - t0 > tmax) return -1;
        }
        return rows.size() > before ? 2 : 0;
    }
};

static int cmd_pc(int dmin, int dmax, double tmax, double memgb, int voll) {
    int k; auto C = readcnf(k); double t0 = now(); size_t peak = 0, last = 0; long lneu = 0, lrund = 0;
    for (auto& c : C) dmin = max(dmin, (int)c.size());
    for (int d = dmin; d <= dmax; d++) {
        PC P(k, d); P.voll = voll; P.memcap = (size_t)(memgb * 1e9); int res = P.run(C, t0, tmax);
        size_t mb = (P.bytes + 8 * (size_t)P.N + 4 * P.mul.size()) >> 20; peak = max(peak, mb);
        last = P.rows.size(); lneu = P.vneu; lrund = P.runden;
        if (res != 0) { printf("%d %d %zu %.3f %zu %ld %ld\n", d, res == 1 ? 0 : (res == -1 ? 1 : 2), P.rows.size(), now() - t0, peak, P.vneu, P.runden); return 0; }
    }
    printf("%d 0 %zu %.3f %zu %ld %ld\n", dmax + 1, last, now() - t0, peak, lneu, lrund);
    return 0;
}

int main(int argc, char** argv) {
    ios::sync_with_stdio(false);
    if (argc >= 2 && !strcmp(argv[1], "mus")) return cmd_mus();
    if (argc >= 5 && !strcmp(argv[1], "pc")) return cmd_pc(atoi(argv[2]), atoi(argv[3]), atof(argv[4]), argc >= 6 ? atof(argv[5]) : 4.0, argc >= 7 ? atoi(argv[6]) : 0);
    fprintf(stderr, "Aufruf: m12pc mus | m12pc pc dmin dmax tmax [memgb] [voll]\n"); return 2;
}