#include <climits>
/*******************************************************************************
 * Satori - SAT Solver for planning-style binary-dense CNF instances (v.50)
 *
 * Copyright (c) 2026 Massimo Di Gruso <license@satori-sat.com>
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 *
 * Build (dynamic — RECOMMENDED; this is the recipe used for the benchmarks):
 *   g++ -O2 -fno-exceptions -fno-rtti -DNDEBUG -o satori satori.cpp
 *   Notes (measured on the planning corpus):
 *     - -O3 and -march=native give NO benefit over -O2 (within run-to-run noise).
 *     - -Os makes the binary ~38% smaller but 25-45% slower; not recommended.
 *
 * Build (static — self-contained binary for embedded/musl deployment):
 *   g++ -O2 -fno-exceptions -fno-rtti -DNDEBUG -static -s -o satori satori.cpp
 *   (On armv6l/Alpine the dynamic build was used; -static is optional.)
 *
 * Usage:
 *   ./satori <file.cnf>
 ******************************************************************************/

#include <iostream>
#include <fstream>
#include <vector>
#include <unordered_map>
#include <string>
#include <queue>
#include <chrono>
#include <algorithm>
#include <cstdio>
#include <cstring>
#include <cctype>
#include <cstdint>
#include <cmath>

using namespace std;

static inline int lit_idx_of(int signed_lit) {
    return signed_lit > 0 ? (signed_lit << 1) : (((-signed_lit) << 1) | 1);
}
static inline int var_of(int lit_idx) { return lit_idx >> 1; }
static inline int neg_of(int lit_idx) { return lit_idx ^ 1; }
static inline bool is_pos(int lit_idx) { return (lit_idx & 1) == 0; }

struct VSIDSHeap {
    vector<int>    heap;
    vector<int>    pos;
    vector<float>* act;

    void init(int n_vars, vector<float>* activity) {
        act = activity;
        heap.clear();
        pos.assign(n_vars + 1, -1);
    }

    bool empty() const { return heap.empty(); }
    int  size()  const { return (int)heap.size(); }
    bool contains(int v) const { return pos[v] != -1; }

    void sift_up(int i) {
        int v = heap[i];
        while (i > 0) {
            int parent = (i - 1) >> 1;
            int pv = heap[parent];
            if ((*act)[v] > (*act)[pv]) {
                heap[i] = pv;
                pos[pv] = i;
                i = parent;
            } else break;
        }
        heap[i] = v;
        pos[v] = i;
    }

    void sift_down(int i) {
        int n = (int)heap.size();
        int v = heap[i];
        while (true) {
            int l = 2*i + 1, r = 2*i + 2, best = i;
            int best_v = v;
            if (l < n && (*act)[heap[l]] > (*act)[best_v]) { best = l; best_v = heap[l]; }
            if (r < n && (*act)[heap[r]] > (*act)[best_v]) { best = r; best_v = heap[r]; }
            if (best == i) break;
            heap[i] = best_v;
            pos[best_v] = i;
            i = best;
        }
        heap[i] = v;
        pos[v] = i;
    }

    void insert(int v) {
        if (pos[v] != -1) return;
        pos[v] = (int)heap.size();
        heap.push_back(v);
        sift_up(pos[v]);
    }

    int extract_max() {
        if (heap.empty()) return -1;
        int top = heap[0];
        int last = heap.back();
        heap.pop_back();
        pos[top] = -1;
        if (!heap.empty()) {
            heap[0] = last;
            pos[last] = 0;
            sift_down(0);
        }
        return top;
    }

    void increase(int v) {
        if (pos[v] == -1) return;
        sift_up(pos[v]);
    }
};

class SatoriCDCL {
public:

    string cnf_file;
    int    num_vars = 0;
    int    num_clauses_input = 0;

    vector<int32_t>         lit_arena;
    vector<uint32_t>        cl_begin;
    vector<uint32_t>        cl_size;

    inline int32_t*       cl_data(int cid)       { return lit_arena.data() + cl_begin[cid]; }
    inline const int32_t* cl_data(int cid) const { return lit_arena.data() + cl_begin[cid]; }
    inline uint32_t       cl_len (int cid) const { return cl_size[cid]; }
    inline int            cl_count() const       { return (int)cl_begin.size(); }

    // Unified watch list (one per literal) with blocking literal.
    //   cid >= 0 : long clause (len >= 3) stored in the arena; 'blocker'
    //              is a cached literal — if true the clause is satisfied
    //              and the arena is never touched.
    //   cid == -1: binary clause stored INLINE; 'blocker' is the other
    //              literal. Binary clauses never live in the arena at all
    //              (saves ~21 bytes/clause) and a single merged list halves
    //              the vector-header overhead of two parallel structures.
    struct Watch { int32_t cid; int32_t blocker; };
    static const int32_t BIN_CID = -1;
    vector<vector<Watch>>   watches;

    // Binary reasons/conflicts are encoded as literals, not clause refs:
    //   reason[v] = -4 - other_lit   (other_lit = the false partner)
    static inline int  enc_bin(int lit)  { return -4 - lit; }
    static inline int  dec_bin(int code) { return -4 - code; }
    static inline bool is_bin_code(int code) { return code <= -4; }
    int                     confl_bin_second = 0;  // 2nd lit of a binary conflict

    int                     n_problem_clauses = 0;  // LONG problem clauses in arena
    long long               n_clauses_added  = 0;   // all problem clauses (incl. binaries)
    long long               n_binary_clauses = 0;   // problem binaries

    vector<int>             lbd;
    vector<uint8_t>         removed;
    int                     max_learnts = 0;
    int                     n_learnts_alive = 0;
    int                     n_reductions = 0;
    double                  learnts_growth = 1.1;

    vector<int8_t>          assignment;
    vector<int>             level;
    vector<int>             reason;
    vector<int>             trail;
    vector<int>             trail_lim;
    int                     qhead = 0;

    vector<float>           activity;
    double                  var_inc = 1.0;
    double                  var_decay = 0.95;

    // --- satori-49: temporal decision priority (early-layer + implication-source)
    // tprio[v] in [-1,1]: high = early time layer and/or an implication SOURCE
    // (antecedent of x->y binary clauses); low = late and/or a passive SINK that
    // unit propagation determines anyway. A persistent "forward kick" re-applied
    // at each restart keeps these variables on top of the heap instead of letting
    // VSIDS wash the initial seed out. Gated on temporal_banded; tunable via env.
    vector<float>           tprio;
    bool                    s49_on    = true;   // SATORI49=off disables
    float                   s49_early = 1.0f;   // SATORI49_EARLY weight
    float                   s49_src   = 0.5f;   // SATORI49_SRC   weight
    float                   s49_kick  = 0.3f;   // SATORI49_KICK  restart kick scale
    float                   s50_span  = 1.0f;   // SATORI50_SPAN  weight (ON by default; the validated span heuristic)
    vector<int>             vspan;              // per-var neighbour-index span (raw)
    void s49_read_env() {
        if (const char* e = getenv("SATORI49"))       s49_on   = string(e) != "off";
        if (const char* e = getenv("SATORI49_EARLY")) s49_early = atof(e);
        if (const char* e = getenv("SATORI49_SRC"))   s49_src   = atof(e);
        if (const char* e = getenv("SATORI49_KICK"))  s49_kick  = atof(e);
        if (const char* e = getenv("SATORI50_SPAN"))  s50_span  = atof(e);
    }
    VSIDSHeap               order_heap;

    vector<int8_t>          phase;

    long long n_decisions = 0;
    long long n_conflicts = 0;
    long long n_propagations = 0;
    long long n_learned = 0;
    long long n_restarts = 0;
    double    parse_time = 0.0;
    double    solve_time = 0.0;

    int        restart_base = 100;

    // --- LBD-based adaptive restart (Glucose-style), gated by size ---
    // Active only when n_problem_clauses >= adaptive_restart_gate; below
    // the gate the proven Luby strategy is used unchanged (doc note (f):
    // LBD restart is the first improvement for >200K-clause instances).
    bool       adaptive_restart = false;
    int        adaptive_restart_gate = 0;        // clauses: LBD restarts always on (UNSAT speed; SAT family verified unchanged)
    double     restart_K = 0.8;    // restart if recent_avg * K > global_avg
    double     restart_R = 1.4;    // block if trail > R * trail_avg
    static const int LBD_QUEUE_CAP   = 50;
    static const int TRAIL_QUEUE_CAP = 5000;
    int        lbd_queue[LBD_QUEUE_CAP];
    int        lbd_q_n = 0, lbd_q_i = 0;
    long long  lbd_q_sum = 0;
    double     lbd_global_sum = 0.0;
    int        trail_queue[TRAIL_QUEUE_CAP];
    int        trail_q_n = 0, trail_q_i = 0;
    long long  trail_q_sum = 0;

    inline void lbd_queue_clear() { lbd_q_n = 0; lbd_q_i = 0; lbd_q_sum = 0; }
    inline void lbd_queue_push(int x) {
        if (lbd_q_n < LBD_QUEUE_CAP) { lbd_q_n++; }
        else { lbd_q_sum -= lbd_queue[lbd_q_i]; }
        lbd_queue[lbd_q_i] = x;
        lbd_q_sum += x;
        lbd_q_i = (lbd_q_i + 1) % LBD_QUEUE_CAP;
    }
    inline void trail_queue_push(int x) {
        if (trail_q_n < TRAIL_QUEUE_CAP) { trail_q_n++; }
        else { trail_q_sum -= trail_queue[trail_q_i]; }
        trail_queue[trail_q_i] = x;
        trail_q_sum += x;
        trail_q_i = (trail_q_i + 1) % TRAIL_QUEUE_CAP;
    }

    void var_bump(int v) {
        activity[v] += var_inc;
        if (activity[v] > 1e30f) {

            for (int i = 1; i <= num_vars; i++) activity[i] *= 1e-30f;
            var_inc *= 1e-30;
        }
        order_heap.increase(v);
    }
    void var_decay_act() { var_inc *= (1.0 / var_decay); }

    inline int  decision_level() const { return (int)trail_lim.size(); }
    inline int8_t lit_value(int lit_idx) const {
        int v = var_of(lit_idx);
        int8_t a = assignment[v];
        if (a == 0) return 0;

        return is_pos(lit_idx) ? a : (int8_t)-a;
    }

    vector<uint8_t>         is_head;
    vector<int>             siblings_csr;
    vector<uint32_t>        siblings_off;
    vector<int>             head_of_var;
    long long               n_heads = 0;
    long long               n_sibling_pairs = 0;
    bool                    planning_pattern_detected = false;

    inline const int* sib_data(int v) const { return siblings_csr.data() + siblings_off[v]; }
    inline int        sib_len (int v) const { return (int)(siblings_off[v+1] - siblings_off[v]); }

    vector<int>             lit_remap;
    long long               n_scc_subst_vars = 0;

    long long               n_scc_bin_removed = 0;

    // Flat CSR copy of the original clauses, kept only when SCC
    // substitution rewrites the formula (needed for model verification).
    // A vector<vector<int>> here costs ~40-60 extra bytes per clause in
    // headers + allocator overhead; CSR is exactly the literal data.
    vector<int32_t>         verify_lits;
    vector<uint32_t>        verify_off;
    bool                    scc_applied = false;


    void detect_planning_pattern_arena(const vector<int32_t>& raw_lits,
                                       const vector<uint32_t>& raw_off,
                                       int n_raw)
    {
        is_head     .assign(num_vars + 1, 0);
        head_of_var .assign(num_vars + 1, 0);

        int n_long_total = 0;
        int n_pattern    = 0;
        vector<pair<int,int>> pairs;
        pairs.reserve(n_raw * 4);

        for (int i = 0; i < n_raw; i++) {
            uint32_t a = raw_off[i], b = raw_off[i+1];
            int sz = (int)(b - a);
            if (sz < 3) continue;
            n_long_total++;

            int neg_lit = 0;
            int neg_count = 0;
            bool ok = true;
            for (uint32_t k = a; k < b; k++) {
                int li = raw_lits[k];
                if (!is_pos(li)) {
                    neg_lit = li;
                    neg_count++;
                    if (neg_count > 1) { ok = false; break; }
                }
            }
            if (!ok || neg_count != 1) continue;
            n_pattern++;

            int x_var = var_of(neg_lit);
            is_head[x_var] = 1;

            int ny = 0;
            int ys_local[64];
            vector<int> ys_overflow;
            for (uint32_t k = a; k < b; k++) {
                int li = raw_lits[k];
                if (is_pos(li)) {
                    int yv = var_of(li);
                    if (head_of_var[yv] == 0) head_of_var[yv] = x_var;
                    if (ny < 64) ys_local[ny++] = yv;
                    else ys_overflow.push_back(yv);
                }
            }
            int total_ys = ny + (int)ys_overflow.size();
            auto get_y = [&](int i) { return i < ny ? ys_local[i] : ys_overflow[i - ny]; };
            for (int i2 = 0; i2 < total_ys; i2++) {
                int y = get_y(i2);
                for (int j = 0; j < total_ys; j++) {
                    if (i2 == j) continue;
                    pairs.emplace_back(y, get_y(j));
                }
            }
        }

        sort(pairs.begin(), pairs.end());
        pairs.erase(unique(pairs.begin(), pairs.end()), pairs.end());

        siblings_off.assign(num_vars + 2, 0);
        for (const auto& p : pairs) siblings_off[p.first + 1]++;
        for (int v = 1; v <= num_vars + 1; v++) siblings_off[v] += siblings_off[v-1];
        siblings_csr.assign(pairs.size(), 0);
        vector<uint32_t> cur(num_vars + 2, 0);
        for (int v = 0; v <= num_vars + 1; v++) cur[v] = siblings_off[v];
        for (const auto& p : pairs) {
            siblings_csr[cur[p.first]++] = p.second;
        }
        n_sibling_pairs = (long long)pairs.size();

        for (int v = 1; v <= num_vars; v++) if (is_head[v]) n_heads++;

        if (n_long_total > 0 && (double)n_pattern / n_long_total >= 0.05) {
            planning_pattern_detected = true;
        }
        if (n_heads >= 50) planning_pattern_detected = true;
    }

    bool compute_scc_leaders_arena_with_budget(
            const vector<int32_t>& raw_lits,
            const vector<uint32_t>& raw_off,
            int n_raw,
            vector<int>& leader_out,
            chrono::time_point<chrono::high_resolution_clock> t_start,
            double budget_sec)
    {
        int N = 2 * (num_vars + 1);

        vector<uint32_t> head_off(N + 1, 0);
        size_t n_arcs = 0;
        for (int i = 0; i < n_raw; i++) {
            if (raw_off[i+1] - raw_off[i] != 2) continue;
            int a = raw_lits[raw_off[i]], b = raw_lits[raw_off[i]+1];
            head_off[neg_of(a) + 1]++;
            head_off[neg_of(b) + 1]++;
            n_arcs += 2;
        }
        for (int k = 1; k <= N; k++) head_off[k] += head_off[k-1];
        vector<int32_t> adj_csr(n_arcs);
        vector<uint32_t> cur(N, 0);
        for (int k = 0; k < N; k++) cur[k] = head_off[k];
        for (int i = 0; i < n_raw; i++) {
            if (raw_off[i+1] - raw_off[i] != 2) continue;
            int a = raw_lits[raw_off[i]], b = raw_lits[raw_off[i]+1];
            adj_csr[cur[neg_of(a)]++] = b;
            adj_csr[cur[neg_of(b)]++] = a;
        }
        vector<uint32_t>().swap(cur);

        const int BUDGET_CHECK_INTERVAL = 10000;
        int ops_since_check = 0;

        vector<int> index(N, -1), lowlink(N, 0), stk;
        vector<uint8_t> on_stack(N, 0);
        leader_out.assign(N, -1);
        int idx_counter = 0;

        struct Frame { int v; int it; };
        vector<Frame> call_stack;

        for (int start = 0; start < N; start++) {
            if (index[start] != -1) continue;
            call_stack.push_back({start, 0});
            index[start] = idx_counter;
            lowlink[start] = idx_counter;
            idx_counter++;
            stk.push_back(start);
            on_stack[start] = 1;

            while (!call_stack.empty()) {
                if (++ops_since_check >= BUDGET_CHECK_INTERVAL) {
                    ops_since_check = 0;
                    double elapsed = chrono::duration<double>(
                        chrono::high_resolution_clock::now() - t_start).count();
                    if (elapsed > budget_sec) {
                        leader_out.clear();
                        return false;
                    }
                }
                Frame& f = call_stack.back();
                int v = f.v;
                int v_deg = (int)(head_off[v+1] - head_off[v]);
                if (f.it < v_deg) {
                    int w = adj_csr[head_off[v] + f.it++];
                    if (index[w] == -1) {
                        index[w] = idx_counter;
                        lowlink[w] = idx_counter;
                        idx_counter++;
                        stk.push_back(w);
                        on_stack[w] = 1;
                        call_stack.push_back({w, 0});
                    } else if (on_stack[w]) {
                        lowlink[v] = min(lowlink[v], index[w]);
                    }
                } else {
                    if (lowlink[v] == index[v]) {
                        int leader = -1;
                        vector<int> scc_members;
                        while (true) {
                            int w = stk.back(); stk.pop_back();
                            on_stack[w] = 0;
                            scc_members.push_back(w);
                            if (leader == -1 || w < leader) leader = w;
                            if (w == v) break;
                        }

                        for (int w : scc_members) {
                            for (int u : scc_members) {
                                if (u == neg_of(w)) {
                                    leader_out.assign(N, 0);
                                    return false;
                                }
                            }
                        }
                        for (int w : scc_members) leader_out[w] = leader;
                    }
                    int popped = f.v;
                    call_stack.pop_back();
                    if (!call_stack.empty()) {
                        int parent = call_stack.back().v;
                        lowlink[parent] = min(lowlink[parent], lowlink[popped]);
                    }
                }
            }
        }
        return true;
    }

    bool add_clause_initial(vector<int>& lits) {

        sort(lits.begin(), lits.end());
        lits.erase(unique(lits.begin(), lits.end()), lits.end());
        for (size_t i = 0; i + 1 < lits.size(); i++) {
            if (lits[i] == neg_of(lits[i+1])) {

                return true;
            }
        }
        if (lits.empty()) return false;
        if (lits.size() == 1) {

            int8_t v = lit_value(lits[0]);
            if (v == 1) return true;
            if (v == -1) return false;
            int var = var_of(lits[0]);
            int val = is_pos(lits[0]) ? 1 : -1;
            assignment[var] = (int8_t)val;
            level[var] = 0;
            reason[var] = -2;
            trail.push_back(var);
            return true;
        }

        if (lits.size() == 2) {
            n_clauses_added++;
            n_binary_clauses++;
            watches[lits[0]].push_back({BIN_CID, (int32_t)lits[1]});
            watches[lits[1]].push_back({BIN_CID, (int32_t)lits[0]});
            return true;
        }

        int cid = cl_count();
        n_clauses_added++;
        cl_begin.push_back((uint32_t)lit_arena.size());
        cl_size .push_back((uint32_t)lits.size());
        for (int li : lits) lit_arena.push_back(li);
        lbd.push_back(0);
        removed.push_back(0);
        watches[lits[0]].push_back({(int32_t)cid, (int32_t)lits[1]});
        watches[lits[1]].push_back({(int32_t)cid, (int32_t)lits[0]});
        return true;
    }

    // Long learnt clauses only (size >= 3). Learnt binaries are attached
    // directly to the merged watch lists in the solve loop.
    int add_learned_clause(vector<int>& lits, int learnt_lbd) {
        int cid = cl_count();
        cl_begin.push_back((uint32_t)lit_arena.size());
        cl_size .push_back((uint32_t)lits.size());
        for (int li : lits) lit_arena.push_back(li);
        lbd.push_back(learnt_lbd);
        removed.push_back(0);
        n_learnts_alive++;
        watches[lits[0]].push_back({(int32_t)cid, (int32_t)lits[1]});
        watches[lits[1]].push_back({(int32_t)cid, (int32_t)lits[0]});
        return cid;
    }

    bool parse_cnf() {
        auto t0 = chrono::high_resolution_clock::now();
        FILE* f = fopen(cnf_file.c_str(), "r");
        if (!f) { cerr << "ERROR: cannot open " << cnf_file << endl; exit(1); }

        char buffer[65536];
        bool header_seen = false;

        vector<int32_t>  raw_lits;
        vector<uint32_t> raw_off;
        raw_off.push_back(0);

        while (fgets(buffer, sizeof(buffer), f)) {
            char* line = buffer;
            while (*line==' '||*line=='\t'||*line=='\r'||*line=='\n') line++;
            if (*line == '\0' || *line == 'c') continue;
            if (!header_seen && strncmp(line, "p cnf", 5) == 0) {
                sscanf(line, "p cnf %d %d", &num_vars, &num_clauses_input);
                header_seen = true;

                raw_lits.reserve(num_clauses_input * 3);
                raw_off .reserve(num_clauses_input + 1);
                continue;
            }
            char* ptr = line;
            while (*ptr) {
                while (*ptr && (*ptr==' '||*ptr=='\t'||*ptr=='\r'||*ptr=='\n')) ptr++;
                if (!*ptr) break;
                bool neg = (*ptr == '-');
                if (neg) ptr++;
                if (!isdigit((unsigned char)*ptr)) break;
                int x = 0;
                while (isdigit((unsigned char)*ptr)) { x = x*10 + (*ptr - '0'); ptr++; }
                if (x == 0) {

                    if (raw_off.back() != raw_lits.size()) {
                        raw_off.push_back((uint32_t)raw_lits.size());
                    }
                } else {
                    int signed_lit = neg ? -x : x;
                    raw_lits.push_back(lit_idx_of(signed_lit));
                }
            }
        }
        if (raw_off.back() != raw_lits.size()) {
            raw_off.push_back((uint32_t)raw_lits.size());
        }
        fclose(f);

        int n_raw = (int)raw_off.size() - 1;

        assignment.assign(num_vars + 1, 0);
        level     .assign(num_vars + 1, -1);
        reason    .assign(num_vars + 1, -1);
        activity  .assign(num_vars + 1, 0.0f);
        phase     .assign(num_vars + 1, -1);
        watches   .assign(2 * (num_vars + 1), {});
        trail.reserve(num_vars);

        order_heap.init(num_vars, &activity);

        // Diagnostica di buona-posizione del problema (debug encoder)
        if (getenv("SATORI_LINT"))
            lint_pass(raw_lits, raw_off, n_raw, num_vars, num_clauses_input);

        {
            int n_bin_pre = 0;
            for (int i = 0; i < n_raw; i++) if (raw_off[i+1] - raw_off[i] == 2) n_bin_pre++;
            double bin_ratio = (double)n_bin_pre / max(1, n_raw);
            // SCC substitution rewrites the formula: incompatible with
            // DRAT emission (the proof must refer to the original CNF),
            // so it is disabled when a proof file is requested.
            if (!drat && n_raw >= 10000 && bin_ratio >= 0.85) {
                auto t_scc_start = chrono::high_resolution_clock::now();
                vector<int> leader;
                bool ok = compute_scc_leaders_arena_with_budget(
                    raw_lits, raw_off, n_raw, leader, t_scc_start, 0.005);
                if (!ok) {
                    if (!leader.empty()) {
                        parse_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
                        return false;
                    }

                } else {
                    bool any_nontrivial = false;
                    for (int li = 0; li < (int)leader.size(); li++) {
                        if (leader[li] != -1 && leader[li] != li) { any_nontrivial = true; break; }
                    }
                    if (any_nontrivial) {

                        scc_applied = true;
                        verify_lits = raw_lits;          // flat copy
                        verify_off  = raw_off;

                        lit_remap.assign(2 * (num_vars + 1), 0);
                        for (int li = 0; li < (int)lit_remap.size(); li++) {
                            lit_remap[li] = (leader[li] != -1) ? leader[li] : li;
                        }
                        for (int v = 1; v <= num_vars; v++) {
                            int pos = v << 1;
                            if (lit_remap[pos] != pos) n_scc_subst_vars++;
                        }

                        size_t orig_bin = 0, kept_bin = 0;
                        vector<int32_t>  raw_lits2;
                        vector<uint32_t> raw_off2;
                        raw_lits2.reserve(raw_lits.size());
                        raw_off2 .reserve(raw_off.size());
                        raw_off2.push_back(0);
                        bool unsat = false;
                        vector<int> tmp_cl;
                        for (int i = 0; i < n_raw; i++) {
                            uint32_t a = raw_off[i], b = raw_off[i+1];
                            if (b - a == 2) orig_bin++;
                            tmp_cl.assign(raw_lits.data() + a, raw_lits.data() + b);
                            for (auto& li : tmp_cl) li = lit_remap[li];
                            sort(tmp_cl.begin(), tmp_cl.end());
                            tmp_cl.erase(unique(tmp_cl.begin(), tmp_cl.end()), tmp_cl.end());
                            bool taut = false;
                            for (size_t k = 0; k + 1 < tmp_cl.size(); k++) {
                                if (tmp_cl[k] == neg_of(tmp_cl[k+1])) { taut = true; break; }
                            }
                            if (taut) continue;
                            if (tmp_cl.empty()) { unsat = true; break; }
                            if (tmp_cl.size() == 2) kept_bin++;
                            for (int li : tmp_cl) raw_lits2.push_back(li);
                            raw_off2.push_back((uint32_t)raw_lits2.size());
                        }
                        if (unsat) {
                            parse_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
                            return false;
                        }
                        n_scc_bin_removed = (long long)orig_bin - (long long)kept_bin;
                        raw_lits = std::move(raw_lits2);
                        raw_off  = std::move(raw_off2);
                        n_raw    = (int)raw_off.size() - 1;
                    }
                }
            }
        }


        // The sibling structure is consumed ONLY by failed-literal probing,
        // which is gated on (>=10K clauses, >=85% binary). Building it on
        // instances that fail the gate (e.g. blocks-world, ~70% binary) is
        // pure waste: an O(sum len^2) pair enumeration + a large sort.
        {
            int n_bin_pre2 = 0;
            for (int i = 0; i < n_raw; i++) if (raw_off[i+1] - raw_off[i] == 2) n_bin_pre2++;
            double br = (double)n_bin_pre2 / max(1, n_raw);
            if (n_raw >= 10000 && br >= 0.85)
                detect_planning_pattern_arena(raw_lits, raw_off, n_raw);
        }

        for (int i = 0; i < n_raw; i++) {
            uint32_t a = raw_off[i], b = raw_off[i+1];
            int len = (int)(b - a);
            if (len == 0) continue;
            int neg_count = 0;
            bool all_neg = true;
            for (uint32_t k = a; k < b; k++) {
                if (!is_pos(raw_lits[k])) neg_count++;
                else all_neg = false;
            }
            double w = 1.0 / max(1, len);
            if (all_neg) w *= 2.0;
            else if (neg_count == 1) {
                if (len <= 3) w *= 2.5;
                else if (len <= 5) w *= 1.5;
            }
            for (uint32_t k = a; k < b; k++) activity[var_of(raw_lits[k])] += w;
        }

        // Portfolio diversification: tiny multiplicative jitter on the
        // initial activities (SATORI_SEED=n). Trajectory variance measured
        // on this family is 2-4x between near-identical configurations:
        // a portfolio pays min(runs) instead of the mean, so cheap
        // diversification is the most effective lever available.
        if (const char* se = getenv("SATORI_SEED")) {
            uint64_t s = (uint64_t)atoll(se) * 0x9E3779B97F4A7C15ull + 0xD1B54A32D192ED03ull;
            for (int v = 1; v <= num_vars; v++) {
                s ^= s >> 12; s ^= s << 25; s ^= s >> 27;
                double r = (double)((s * 0x2545F4914F6CDD1Dull) >> 40) / (double)(1ull << 24);
                activity[v] *= (1.0 + 0.10 * r);   // jitter 0..10%
            }
        }

        // ---- Temporal band detection + forward ramp ----
        // Planning encoders (SATPLAN/Graphplan family) number variables by
        // time layer, so binary clauses (mutexes, action->precondition/
        // effect links) connect variables that are CLOSE in index: the
        // adjacency structure is a narrow band. We detect this via the 90th
        // percentile of |var_i - var_j| over binary clauses. When the
        // formula is banded, bias initial activity toward LOW indices
        // (early time layers): with default-false phases, decisions then
        // build the plan forward in time with minimal commitment, so
        // contradictions with the "story" surface early and near the trail
        // root, where learnt clauses prune the most. (The backward ramp was
        // also tested: it helps occasionally on blocks-world but badly
        // hurts logistics-style instances; forward is the only direction
        // that is consistent across families: ~0.90x geomean time.)
        s49_read_env();
        temporal_banded = false;
        {
            vector<int> gaps;
            gaps.reserve(n_raw);
            vector<int> outdeg(num_vars + 1, 0), indeg(num_vars + 1, 0); // s49: implication direction
            long long n_bin2 = 0, n_mutex = 0;     // (N,N) = mutex, simmetrici
            for (int i = 0; i < n_raw; i++) {
                if (raw_off[i+1] - raw_off[i] != 2) continue;
                int la = raw_lits[raw_off[i]], lb = raw_lits[raw_off[i] + 1];
                int va = var_of(la), vb = var_of(lb);
                gaps.push_back(va > vb ? va - vb : vb - va);
                n_bin2++;
                bool na = !is_pos(la), nb = !is_pos(lb);
                if (!na && !nb) {}                                  // (P,P)
                else if (na && nb) n_mutex++;                       // (N,N) mutex
                else if (na && !nb) { outdeg[va]++; indeg[vb]++; }  // va -> vb
                else                { outdeg[vb]++; indeg[va]++; }  // vb -> va
            }
            if ((int)gaps.size() >= 1000) {
                size_t p = gaps.size() * 9 / 10;
                nth_element(gaps.begin(), gaps.begin() + p, gaps.end());
                band_p90 = gaps[p];
                if ((double)band_p90 <= 0.15 * num_vars) {
                    temporal_banded = true;
                    mutex_frac = (double)n_mutex / max(1LL, n_bin2);
                    const char* ramp_env = getenv("SATORI_RAMP");
                    bool force_off    = ramp_env && string(ramp_env) == "off";
                    bool force_fwd    = ramp_env && string(ramp_env) == "forward";
                    bool force_center = ramp_env && string(ramp_env) == "center";
                    if (force_off) { temporal_banded = true; /* banda nota, rampa no */ }
                    else
                    // The ramp SHAPE depends on the anisotropy of the
                    // binary structure (measured, see sweep_s41_vs_s42):
                    //  - implication-dominated (N,P) formulas have a strong
                    //    propagation direction: a FORWARD ramp (early time
                    //    layers first) is the only consistent winner;
                    //    center/V/comb all lose ~18%.
                    //  - mutex-dominated (N,N) formulas are symmetric, no
                    //    privileged direction: a CENTER peak wins (~11%) by
                    //    propagating in both temporal directions at once,
                    //    splitting the instance around the middle state.
                    if (force_center || (!force_fwd && mutex_frac >= 0.70)) {
                        for (int v = 1; v <= num_vars; v++) {
                            double t = (double)v / num_vars;
                            activity[v] *= (1.0 + 0.5 * (1.0 - fabs(t - 0.5) * 2.0));
                        }
                    } else if (s49_on) {
                        // satori-49/50: implication-dominated forward priority.
                        // tprio = early-layer + source-vs-sink (+ optional span).
                        int maxd = 1;
                        for (int v = 1; v <= num_vars; v++)
                            maxd = max(maxd, abs(outdeg[v] - indeg[v]));
                        // satori-50: per-variable neighbour-index span (independent axis)
                        int maxspan = 1;
                        if (s50_span != 0.0f) {
                            vspan.assign(num_vars + 1, 0);
                            vector<int> nmn(num_vars + 1, INT_MAX), nmx(num_vars + 1, 0);
                            for (int i = 0; i < n_raw; i++) {
                                int b = raw_off[i], e = raw_off[i+1], lo = num_vars+1, hi = 0;
                                for (int j = b; j < e; j++) { int a = var_of(raw_lits[j]); if (a<lo) lo=a; if (a>hi) hi=a; }
                                for (int j = b; j < e; j++) { int a = var_of(raw_lits[j]); if (lo<nmn[a]) nmn[a]=lo; if (hi>nmx[a]) nmx[a]=hi; }
                            }
                            for (int v = 1; v <= num_vars; v++)
                                if (nmx[v] > 0) { vspan[v] = nmx[v]-nmn[v]; if (vspan[v]>maxspan) maxspan=vspan[v]; }
                        }
                        tprio.assign(num_vars + 1, 0.0f);
                        for (int v = 1; v <= num_vars; v++) {
                            float early = 1.0f - (float)v / num_vars;          // 1 .. 0
                            float src   = (float)(outdeg[v] - indeg[v]) / maxd; // -1 .. 1
                            float span  = (s50_span != 0.0f) ? (float)vspan[v] / maxspan : 0.0f; // 0 .. 1
                            tprio[v] = s49_early * early + s49_src * src + s50_span * span;
                        }
                        // stronger-than-legacy initial seed from tprio (clamped)
                        for (int v = 1; v <= num_vars; v++) {
                            float f = 1.0f + 0.5f * tprio[v];
                            if (f < 0.1f) f = 0.1f; if (f > 3.0f) f = 3.0f;
                            activity[v] *= f;
                        }
                    } else {
                        for (int v = 1; v <= num_vars; v++)
                            activity[v] *= (1.0 + 0.5 * (1.0 - (double)v / num_vars));
                    }
                }
            }
        }

        // (frontier structures are built lazily at the first restart
        // trigger, and only when temporal_banded — see build_frontier_structs)

        for (int v = 1; v <= num_vars; v++)
            order_heap.insert(v);

        vector<int> tmp_lits;
        for (int i = 0; i < n_raw; i++) {
            uint32_t a = raw_off[i], b = raw_off[i+1];
            tmp_lits.assign(raw_lits.data() + a, raw_lits.data() + b);
            if (!add_clause_initial(tmp_lits)) {
                parse_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
                return false;
            }
        }

        vector<int32_t>().swap(raw_lits);
        vector<uint32_t>().swap(raw_off);
        n_problem_clauses = cl_count();   // long problem clauses in the arena
        lit_arena.shrink_to_fit();

        // Watch lists were grown by push_back (up to 2x slack). One trim
        // pass after construction reclaims it; learnt clauses appended
        // later are few compared to the problem clauses.
        for (auto& wl : watches) wl.shrink_to_fit();

        parse_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
        return true;
    }

    // Returns: -1 = no conflict; >= 0 = conflicting long clause cid;
    //          <= -4 = binary conflict, lits = {dec_bin(ret), confl_bin_second}
    int propagate() {
        while (qhead < (int)trail.size()) {
            int v = trail[qhead++];
            int val = assignment[v];

            int false_lit = (val == 1) ? ((v << 1) | 1) : (v << 1);

            vector<Watch>& wl = watches[false_lit];
            int n = (int)wl.size();
            int i = 0, j = 0;

            while (i < n) {
                Watch w = wl[i];

                // Blocking literal: for long clauses it's a cached literal,
                // for binaries it's the OTHER literal — in both cases, if
                // it's true the clause is satisfied and we move on.
                int8_t bval = lit_value(w.blocker);
                if (bval == 1) {
                    wl[j++] = w;
                    i++;
                    continue;
                }

                if (w.cid == BIN_CID) {
                    wl[j++] = w;
                    i++;
                    if (bval == 0) {
                        int uvar = var_of(w.blocker);
                        assignment[uvar] = is_pos(w.blocker) ? (int8_t)1 : (int8_t)-1;
                        level[uvar] = decision_level();
                        reason[uvar] = enc_bin(false_lit);
                        trail.push_back(uvar);
                        n_propagations++;
                        if (assignment[uvar] == 1) fr_assign_true(uvar);
                    } else {
                        // conflict on binary clause {w.blocker, false_lit}
                        confl_bin_second = false_lit;
                        int ret = enc_bin(w.blocker);
                        while (i < n) wl[j++] = wl[i++];
                        wl.resize(j);
                        return ret;
                    }
                    continue;
                }

                int cid = w.cid;
                if (removed[cid]) { i++; continue; }
                int32_t* cl = cl_data(cid);
                int sz = (int)cl_len(cid);

                if (cl[0] == false_lit) std::swap(cl[0], cl[1]);

                int other = cl[0];
                int8_t other_val = lit_value(other);

                if (other_val == 1) {

                    wl[j++] = {(int32_t)cid, (int32_t)other};  // refresh blocker
                    i++;
                    continue;
                }

                int k = 2;
                while (k < sz && lit_value(cl[k]) == -1) k++;
                if (k < sz) {

                    int new_watch = cl[k];
                    cl[1] = new_watch;
                    cl[k] = false_lit;
                    watches[new_watch].push_back({(int32_t)cid, (int32_t)other});

                    i++;
                    continue;
                }

                wl[j++] = {(int32_t)cid, (int32_t)other};
                i++;
                if (other_val == 0) {

                    int uvar = var_of(other);
                    int uval = is_pos(other) ? 1 : -1;
                    assignment[uvar] = (int8_t)uval;
                    level[uvar] = decision_level();
                    reason[uvar] = cid;
                    trail.push_back(uvar);
                    n_propagations++;
                    if (assignment[uvar] == 1) fr_assign_true(uvar);
                } else {

                    while (i < n) wl[j++] = wl[i++];
                    wl.resize(j);
                    return cid;
                }
            }
            wl.resize(j);
        }
        return -1;
    }

    vector<int8_t> seen;
    vector<int>    minimize_keep;   // reusable buffer for ccmin
    void analyze(int conflict_code, vector<int>& out_learnt, int& out_btlevel) {
        if ((int)seen.size() != num_vars + 1) seen.assign(num_vars + 1, 0);

        out_learnt.clear();
        out_learnt.push_back(0);

        int path_count = 0;
        int p = -1;
        int idx = (int)trail.size() - 1;
        int confl = conflict_code;
        int cur_level = decision_level();

        do {
            int32_t  bin_lits[2];
            const int32_t* cl;
            int sz;
            if (confl >= 0) {
                cl = cl_data(confl);
                sz = (int)cl_len(confl);
            } else {
                // Encoded binary clause. For the initial conflict the two
                // literals are {dec_bin(confl), confl_bin_second}; for a
                // reason, they are {p, dec_bin(confl)} (p is skipped below).
                bin_lits[0] = (int32_t)dec_bin(confl);
                bin_lits[1] = (p == -1) ? (int32_t)confl_bin_second : (int32_t)p;
                cl = bin_lits;
                sz = 2;
            }

            for (int kk = 0; kk < sz; kk++) {
                int li = cl[kk];
                if (li == p) continue;
                int v = var_of(li);
                if (!seen[v] && level[v] > 0) {
                    var_bump(v);
                    seen[v] = 1;
                    if (level[v] >= cur_level) {
                        path_count++;
                    } else {
                        out_learnt.push_back(li);
                    }
                }
            }

            while (idx >= 0 && !seen[trail[idx]]) idx--;
            if (idx < 0) {

                break;
            }
            int v = trail[idx];

            p = (assignment[v] == 1) ? (v << 1) : ((v << 1) | 1);
            confl = reason[v];
            seen[v] = 0;
            path_count--;
            idx--;
        } while (path_count > 0);

        int uip_neg = p ^ 1;
        out_learnt[0] = uip_neg;

        // ---- Conflict-clause minimization (MiniSat "deep" mode) ----
        // A literal is redundant if it is implied by the rest of the
        // learnt clause: DFS through its reason graph; succeed only if
        // every path terminates in clause literals or level-0 facts.
        // 'abstract_levels' is a 32-bit level signature used to fail fast.
        {
            analyze_toclear.clear();
            for (size_t k = 1; k < out_learnt.size(); k++)
                analyze_toclear.push_back(var_of(out_learnt[k]));

            uint32_t abstract_levels = 0;
            for (size_t k = 1; k < out_learnt.size(); k++)
                abstract_levels |= 1u << (level[var_of(out_learnt[k])] & 31);

            size_t jj = 1;
            for (size_t k = 1; k < out_learnt.size(); k++) {
                int li = out_learnt[k];
                int v  = var_of(li);
                int r  = reason[v];
                if (r == -1 || r == -2 || !lit_redundant(li, abstract_levels))
                    out_learnt[jj++] = li;
            }
            out_learnt.resize(jj);
        }

        if (out_learnt.size() == 1) {
            out_btlevel = 0;
        } else {
            int max_i = 1;
            int max_lvl = level[var_of(out_learnt[1])];
            for (int k = 2; k < (int)out_learnt.size(); k++) {
                int lv = level[var_of(out_learnt[k])];
                if (lv > max_lvl) { max_lvl = lv; max_i = k; }
            }
            std::swap(out_learnt[1], out_learnt[max_i]);
            out_btlevel = max_lvl;
        }

        for (int v : analyze_toclear) seen[v] = 0;
        seen[var_of(out_learnt[0])] = 0;

        var_decay_act();
    }

    vector<int> analyze_stack;
    vector<int> analyze_toclear;   // vars whose seen[] must be cleared after analyze
    // DFS check: is 'li' implied by the other learnt literals (seen[]) and
    // level-0 facts? Marks visited vars in seen[]/analyze_toclear so
    // repeated queries share work, exactly like MiniSat's litRedundant.
    bool lit_redundant(int li, uint32_t abstract_levels) {
        analyze_stack.clear();
        analyze_stack.push_back(li);
        size_t top = analyze_toclear.size();
        while (!analyze_stack.empty()) {
            int q = analyze_stack.back(); analyze_stack.pop_back();
            int v = var_of(q);
            int r = reason[v];

            int32_t bin_lit;
            const int32_t* cl; int sz;
            if (is_bin_code(r)) {
                bin_lit = (int32_t)dec_bin(r);
                cl = &bin_lit; sz = 1;            // the only "other" literal
            } else {
                cl = cl_data(r); sz = (int)cl_len(r);
            }
            for (int k = 0; k < sz; k++) {
                int pq = cl[k];
                int u  = var_of(pq);
                if (u == v) continue;
                if (!seen[u] && level[u] > 0) {
                    int ru = reason[u];
                    if (ru != -1 && ru != -2 && ((1u << (level[u] & 31)) & abstract_levels)) {
                        seen[u] = 1;
                        analyze_stack.push_back(pq);
                        analyze_toclear.push_back(u);
                    } else {
                        // failed: undo marks made by this query
                        for (size_t t = analyze_toclear.size(); t > top; t--)
                            seen[analyze_toclear[t-1]] = 0;
                        analyze_toclear.resize(top);
                        return false;
                    }
                }
            }
        }
        return true;
    }

    vector<int8_t> level_seen;
    vector<int>    lbd_touched;     // reusable buffer
    int compute_lbd(const vector<int>& cl) {
        if ((int)level_seen.size() < decision_level() + 2)
            level_seen.assign(decision_level() + 2, 0);
        int count = 0;
        lbd_touched.clear();
        for (int li : cl) {
            int lv = level[var_of(li)];
            if (lv < 0) continue;
            if (!level_seen[lv]) {
                level_seen[lv] = 1;
                lbd_touched.push_back(lv);
                count++;
            }
        }
        for (int lv : lbd_touched) level_seen[lv] = 0;
        return count;
    }

    bool is_locked(int cid) {

        if (cl_len(cid) == 0) return false;
        int v = var_of(cl_data(cid)[0]);
        return assignment[v] != 0 && reason[v] == cid;
    }

    void reduce_db() {

        vector<int> learnts;
        learnts.reserve(n_learnts_alive);
        for (int cid = n_problem_clauses; cid < cl_count(); cid++) {
            if (!removed[cid]) learnts.push_back(cid);
        }

        sort(learnts.begin(), learnts.end(),
             [&](int a, int b) {
                 if (lbd[a] != lbd[b]) return lbd[a] < lbd[b];
                 return cl_len(a) < cl_len(b);
             });

        int keep_count = (int)learnts.size() / 2;
        int removed_count = 0;
        for (int idx = keep_count; idx < (int)learnts.size(); idx++) {
            int cid = learnts[idx];
            if (cl_len(cid) <= 2) continue;
            if (lbd[cid] <= 2) continue;
            if (is_locked(cid)) continue;
            drat_delete(cid);
            removed[cid] = 1;
            arena_wasted += cl_len(cid);
            n_learnts_alive--;
            removed_count++;
        }
        n_reductions++;

        max_learnts = (int)(max_learnts * learnts_growth);
        (void)removed_count;

        // Reclaim arena memory once >25% of it is dead literals. Without
        // this, removed clauses stay in the arena forever and RSS grows
        // without bound on long runs (1000s-timeout territory).
        if (arena_wasted * 4 > (long long)lit_arena.size())
            garbage_collect();
    }

    long long arena_wasted = 0;   // literals belonging to removed clauses
    long long n_gc = 0;
    bool temporal_banded = false;
    int  band_p90 = -1;
    double mutex_frac = -1.0;

    // ---- Unexplained-frontier counter (semantic restart blocking) ----
    // A checkpoint clause (~head ∨ p1 ∨ ... ∨ pk, exactly one negative)
    // is an OPEN frontier when head is assigned TRUE but no cause pi is
    // TRUE yet: the story demands an explanation that hasn't been chosen.
    // frontier_open counts open frontiers, maintained incrementally on
    // every TRUE assignment/unassignment. A steadily SHRINKING frontier
    // means the plan is closing: restarting then throws away progress
    // that LBD/trail heuristics cannot see, so we postpone the restart.
    // ---- DRAT proof emission (UNSAT certification) ----
    // Every CDCL-learnt clause (1-UIP + ccmin) and every failed-literal
    // unit is RUP, so the proof is simply the chronological sequence of
    // learnt clauses, deletions, and the final empty clause. Verifiable
    // with an independent checker (drat-trim). SCC substitution rewrites
    // the formula and is therefore DISABLED when a proof is requested.
    FILE* drat = nullptr;
    inline void drat_lit(int li) { fprintf(drat, "%d ", is_pos(li) ? var_of(li) : -var_of(li)); }
    inline void drat_clause(const vector<int>& lits) {
        if (!drat) return;
        for (int li : lits) drat_lit(li);
        fputs("0\n", drat);
    }
    inline void drat_unit(int li) { if (!drat) return; drat_lit(li); fputs("0\n", drat); }
    inline void drat_bin(int a, int b) { if (!drat) return; drat_lit(a); drat_lit(b); fputs("0\n", drat); }
    inline void drat_empty() { if (!drat) return; fputs("0\n", drat); fflush(drat); }
    inline void drat_delete(int cid) {
        if (!drat) return;
        fputs("d ", drat);
        const int32_t* d = cl_data(cid); int sz = (int)cl_len(cid);
        for (int k = 0; k < sz; k++) drat_lit(d[k]);
        fputs("0\n", drat);
    }


    // ============================================================
    // LINT: parse-time well-posedness diagnostics (SATORI_LINT=1)
    // ============================================================
    // Self-contained pass on the raw clause database, run right after
    // reading and BEFORE any preprocessing, so every witness refers to
    // the ORIGINAL 1-based clause ordinals of the input file. Checks:
    //   syntactic : header mismatch, empty clauses, duplicate literals,
    //               tautologies, duplicate clauses, unused variables
    //   logical   : contradictory units, level-0 unit-propagation
    //               conflict (with full derivation chain), binary
    //               equivalence contradiction x ≡ ¬x (with the
    //               implication cycle as a list of clauses)
    void lint_pass(const vector<int32_t>& rl, const vector<uint32_t>& ro,
                   int n_raw, int declared_vars, long long declared_clauses) {
        auto P = [](const char* s) { fprintf(stderr, "c LINT: %s\n", s); };
        char buf[256];
        fprintf(stderr, "c LINT: ================ well-posedness report ================\n");

        // --- sintassi / igiene ---
        if (declared_clauses >= 0 && declared_clauses != n_raw) {
            snprintf(buf, sizeof buf, "header dichiara %lld clausole, trovate %d",
                     declared_clauses, n_raw); P(buf);
        }
        int max_used = 0; vector<uint8_t> used(declared_vars + 1, 0);
        long long taut = 0, duplit = 0, dupcl = 0, empty = 0, units = 0;
        vector<pair<int,int>> unit_list;             // (lit_idx, ordinal)
        unordered_map<uint64_t, int> seen_hash;      // clause hash -> first ordinal
        vector<int32_t> tmp;
        for (int i = 0; i < n_raw; i++) {
            uint32_t a = ro[i], b = ro[i+1];
            if (a == b) { empty++; snprintf(buf, sizeof buf, "clausola %d VUOTA (UNSAT banale)", i+1); P(buf); continue; }
            tmp.assign(rl.begin() + a, rl.begin() + b);
            for (int li : tmp) { int v = var_of(li); if (v > max_used) max_used = v; if (v <= declared_vars) used[v] = 1; }
            sort(tmp.begin(), tmp.end());
            size_t before = tmp.size();
            tmp.erase(unique(tmp.begin(), tmp.end()), tmp.end());
            if (tmp.size() != before) duplit++;
            bool is_taut = false;
            for (size_t k = 0; k + 1 < tmp.size(); k++)
                if (tmp[k+1] == (tmp[k] ^ 1)) { is_taut = true; break; }
            if (is_taut) { taut++; continue; }
            uint64_t h = 1469598103934665603ull;
            for (int li : tmp) { h ^= (uint64_t)(li + 0x9e37); h *= 1099511628211ull; }
            auto it = seen_hash.find(h);
            if (it != seen_hash.end()) dupcl++;
            else seen_hash.emplace(h, i + 1);
            if (tmp.size() == 1) { units++; unit_list.push_back({tmp[0], i + 1}); }
        }
        if (max_used > declared_vars) {
            snprintf(buf, sizeof buf, "variabile %d usata ma header dichiara %d", max_used, declared_vars); P(buf);
        }
        long long unused = 0;
        for (int v = 1; v <= declared_vars; v++) if (!used[v]) unused++;
        snprintf(buf, sizeof buf, "tautologie: %lld | clausole duplicate: %lld | letterali duplicati in clausola: %lld | unita': %lld | var dichiarate ma mai usate: %lld",
                 taut, dupcl, duplit, units, unused); P(buf);

        // --- unita' contraddittorie (testimone diretto) ---
        {
            unordered_map<int,int> upos;   // lit -> ordinal
            for (auto& [li, ord] : unit_list) {
                auto it = upos.find(li ^ 1);
                if (it != upos.end()) {
                    snprintf(buf, sizeof buf, "CONTRADDIZIONE: unita' %s%d (clausola %d) vs %s%d (clausola %d)",
                             is_pos(li ^ 1) ? "" : "-", var_of(li), it->second,
                             is_pos(li) ? "" : "-", var_of(li), ord); P(buf);
                }
                upos.emplace(li, ord);
            }
        }

        // --- BCP a livello 0 con catena di derivazione ---
        {
            // UP counter-based sui raw: reason[v] = ordinale clausola (1-based)
            vector<int8_t> asg(declared_vars + 1, 0);
            vector<int>    why(declared_vars + 1, 0);
            vector<vector<int>> occ(2 * (declared_vars + 1));
            vector<int> unassigned_cnt(n_raw, 0);
            vector<uint8_t> sat_cl(n_raw, 0);
            for (int i = 0; i < n_raw; i++) {
                for (uint32_t k = ro[i]; k < ro[i+1]; k++) {
                    int li = rl[k];
                    if (var_of(li) > declared_vars) continue;
                    occ[li].push_back(i);
                    unassigned_cnt[i]++;
                }
            }
            vector<int> q; q.reserve(64);
            auto assign = [&](int li, int ord) -> bool {
                int v = var_of(li); int8_t val = is_pos(li) ? 1 : -1;
                if (asg[v] == val) return true;
                if (asg[v] == -val) {
                    // conflitto: stampa la catena di derivazione di entrambi
                    snprintf(buf, sizeof buf, "CONFLITTO BCP livello-0 su var %d:", v); P(buf);
                    for (int side = 0; side < 2; side++) {
                        int cur = side == 0 ? why[v] : ord;
                        snprintf(buf, sizeof buf, "  derivazione %s%d <- clausola %d {",
                                 (side==0) == (asg[v]==1) ? "" : "-", v, cur); 
                        string s = buf;
                        if (cur >= 1) for (uint32_t k = ro[cur-1]; k < ro[cur]; k++) {
                            s += (is_pos(rl[k]) ? "" : "-") + to_string(var_of(rl[k])) + " ";
                        }
                        s += "}";
                        fprintf(stderr, "c LINT: %s\n", s.c_str());
                    }
                    return false;
                }
                asg[v] = val; why[v] = ord; q.push_back(li);
                return true;
            };
            bool ok = true;
            for (auto& [li, ord] : unit_list) if (!assign(li, ord)) { ok = false; break; }
            for (size_t qi = 0; ok && qi < q.size(); qi++) {
                int li = q[qi];
                int fl = li ^ 1;
                for (int ci : occ[fl]) {
                    if (sat_cl[ci]) continue;
                    // la clausola ci ha perso un letterale: conta i vivi e l'eventuale forzato
                    int alive = 0, force = -1; bool sat = false;
                    for (uint32_t k = ro[ci]; k < ro[ci+1]; k++) {
                        int lj = rl[k]; int u = var_of(lj);
                        int8_t a2 = (u <= declared_vars) ? asg[u] : 0;
                        if ((is_pos(lj) && a2 == 1) || (!is_pos(lj) && a2 == -1)) { sat = true; break; }
                        if (a2 == 0) { alive++; force = lj; }
                    }
                    if (sat) { sat_cl[ci] = 1; continue; }
                    if (alive == 0) {
                        snprintf(buf, sizeof buf, "CONFLITTO BCP livello-0: clausola %d interamente falsificata dalle unita'", ci+1); P(buf);
                        ok = false; break;
                    }
                    if (alive == 1 && !assign(force, ci + 1)) { ok = false; break; }
                }
            }
            if (ok) {
                snprintf(buf, sizeof buf, "BCP livello-0: chiuso senza conflitti (%zu letterali forzati)", q.size()); P(buf);
            }
        }

        // --- equivalenze binarie: x ≡ ¬x con ciclo testimone ---
        {
            // grafo implicazioni dalle binarie; BFS da ogni unita'... no:
            // cerca cicli l ->* ¬l con BFS limitata dalle componenti: usa
            // un test diretto su un campione di letterali ad alto grado.
            vector<vector<pair<int,int>>> adj(2 * (declared_vars + 1)); // (dest, ordinal)
            for (int i = 0; i < n_raw; i++) {
                if (ro[i+1] - ro[i] != 2) continue;
                int a = rl[ro[i]], b = rl[ro[i]+1];
                if (var_of(a) > declared_vars || var_of(b) > declared_vars) continue;
                adj[a ^ 1].push_back({b, i + 1});
                adj[b ^ 1].push_back({a, i + 1});
            }
            // Tarjan iterativo per trovare una SCC con x e ¬x
            int NL = 2 * (declared_vars + 1);
            vector<int> idx(NL, -1), low(NL, 0), comp(NL, -1), stk;
            vector<uint8_t> onstk(NL, 0);
            int ic = 0, nc = 0;
            struct Fr { int v; size_t it; };
            for (int s = 0; s < NL; s++) {
                if (idx[s] != -1 || adj[s].empty()) continue;
                vector<Fr> cs{{s, 0}};
                idx[s] = low[s] = ic++; stk.push_back(s); onstk[s] = 1;
                while (!cs.empty()) {
                    auto& f = cs.back();
                    if (f.it < adj[f.v].size()) {
                        int w = adj[f.v][f.it++].first;
                        if (idx[w] == -1) {
                            idx[w] = low[w] = ic++; stk.push_back(w); onstk[w] = 1;
                            cs.push_back({w, 0});
                        } else if (onstk[w]) low[f.v] = min(low[f.v], idx[w]);
                    } else {
                        if (low[f.v] == idx[f.v]) {
                            while (true) {
                                int w = stk.back(); stk.pop_back(); onstk[w] = 0;
                                comp[w] = nc;
                                if (w == f.v) break;
                            }
                            nc++;
                        }
                        int v = f.v; cs.pop_back();
                        if (!cs.empty()) low[cs.back().v] = min(low[cs.back().v], low[v]);
                    }
                }
            }
            int bad_lit = -1;
            for (int v = 1; v <= declared_vars && bad_lit < 0; v++)
                if (comp[v<<1] != -1 && comp[v<<1] == comp[(v<<1)|1]) bad_lit = v << 1;
            if (bad_lit >= 0) {
                snprintf(buf, sizeof buf, "CONTRADDIZIONE: var %d equivale alla sua negazione (x = !x). Ciclo testimone:", var_of(bad_lit)); P(buf);
                // BFS bad_lit -> ¬bad_lit e ritorno, stampando le clausole
                for (int leg = 0; leg < 2; leg++) {
                    int from = leg == 0 ? bad_lit : (bad_lit ^ 1);
                    int to   = leg == 0 ? (bad_lit ^ 1) : bad_lit;
                    vector<int> par(NL, -1), pcl(NL, 0);
                    vector<int> bq{from}; par[from] = from;
                    for (size_t qi = 0; qi < bq.size() && par[to] == -1; qi++) {
                        int u = bq[qi];
                        for (auto [w, ord] : adj[u]) if (par[w] == -1) { par[w] = u; pcl[w] = ord; bq.push_back(w); }
                    }
                    if (par[to] == -1) continue;
                    vector<pair<int,int>> path;   // (clausola ord, lit raggiunto)
                    for (int u = to; u != from; u = par[u]) path.push_back({pcl[u], u});
                    for (auto it = path.rbegin(); it != path.rend(); ++it) {
                        snprintf(buf, sizeof buf, "  clausola %d  =>  %s%d", it->first,
                                 is_pos(it->second) ? "" : "-", var_of(it->second)); P(buf);
                    }
                }
            } else {
                P("equivalenze binarie: nessuna contraddizione x = !x");
            }
        }
        fprintf(stderr, "c LINT: ========================================================\n");
    }

    bool             ckpt_enabled = false;
    vector<uint32_t> ck_head_off, ck_head_cl;   // head var  -> clause ids
    vector<uint32_t> ck_cause_off, ck_cause_cl; // cause var -> clause ids
    vector<uint32_t> ck_cl_off;                 // clause -> range in ck_cl_data
    vector<int32_t>  ck_cl_data;                // positive (cause) vars
    vector<int32_t>  ck_ntc;                    // per clause: #true causes
    vector<uint8_t>  ck_head_true;
    long long        frontier_open = 0;
    long long        n_restart_blocks = 0;
    // Glucose-style recent queue of frontier size sampled at conflicts
    static const int FR_QUEUE_CAP = 50;
    long long fr_q[FR_QUEUE_CAP]; int fr_q_n = 0, fr_q_i = 0; long long fr_q_sum = 0;
    inline void fr_queue_push(long long x) {
        if (fr_q_n == FR_QUEUE_CAP) fr_q_sum -= fr_q[fr_q_i]; else fr_q_n++;
        fr_q[fr_q_i] = x; fr_q_sum += x;
        fr_q_i = (fr_q_i + 1) % FR_QUEUE_CAP;
    }
    inline bool frontier_shrinking() {
        return ckpt_enabled && fr_q_n == FR_QUEUE_CAP &&
               (double)frontier_open < 0.9 * ((double)fr_q_sum / FR_QUEUE_CAP);
    }

    bool ckpt_built = false;
    // Lazy build from the ARENA (long problem clauses, exactly one
    // negative literal). Costs nothing — neither memory nor maintenance —
    // until the first conflict at which a restart would actually fire:
    // on instance families where adaptive restarts never trigger
    // (logistics/mixed: avg LBD too low) the frontier machinery is never
    // materialized at all. Measured on the user probe: the eager version
    // cost +9MB RSS and +5-8% time exactly where it never blocked.
    void build_frontier_structs() {
        ckpt_built = true;
        vector<int> hcnt(num_vars + 2, 0), ccnt(num_vars + 2, 0);
        uint32_t ncl = 0;
        for (int cid = 0; cid < n_problem_clauses; cid++) {
            const int32_t* cl = cl_data(cid); int sz = (int)cl_len(cid);
            int neg = -1, nneg = 0;
            for (int k = 0; k < sz; k++)
                if (!is_pos(cl[k])) { nneg++; neg = var_of(cl[k]); }
            if (nneg != 1) continue;
            hcnt[neg]++;
            for (int k = 0; k < sz; k++)
                if (is_pos(cl[k])) ccnt[var_of(cl[k])]++;
            ncl++;
        }
        if (ncl < 100) return;            // troppo poche: non vale
        ckpt_enabled = true;
        ck_head_off.assign(num_vars + 2, 0);
        ck_cause_off.assign(num_vars + 2, 0);
        for (int v = 1; v <= num_vars + 1; v++) {
            ck_head_off[v]  = ck_head_off[v-1]  + hcnt[v-1];
            ck_cause_off[v] = ck_cause_off[v-1] + ccnt[v-1];
        }
        ck_head_cl.resize(ck_head_off[num_vars + 1]);
        ck_cause_cl.resize(ck_cause_off[num_vars + 1]);
        vector<uint32_t> hw(ck_head_off.begin(), ck_head_off.end());
        vector<uint32_t> cw(ck_cause_off.begin(), ck_cause_off.end());
        ck_cl_off.clear(); ck_cl_off.push_back(0);
        ck_cl_data.clear();
        uint32_t cl_i = 0;
        for (int cid = 0; cid < n_problem_clauses; cid++) {
            const int32_t* cl = cl_data(cid); int sz = (int)cl_len(cid);
            int neg = -1, nneg = 0;
            for (int k = 0; k < sz; k++)
                if (!is_pos(cl[k])) { nneg++; neg = var_of(cl[k]); }
            if (nneg != 1) continue;
            ck_head_cl[hw[neg]++] = cl_i;
            for (int k = 0; k < sz; k++)
                if (is_pos(cl[k])) {
                    int u = var_of(cl[k]);
                    ck_cause_cl[cw[u]++] = cl_i;
                    ck_cl_data.push_back(u);
                }
            ck_cl_off.push_back((uint32_t)ck_cl_data.size());
            cl_i++;
        }
        ck_ntc.assign(cl_i, 0);
        ck_head_true.assign(cl_i, 0);
        // stato iniziale dal trail corrente
        frontier_open = 0;
        for (int v : trail) if (assignment[v] == 1) fr_assign_true(v);
        fr_q_n = 0; fr_q_i = 0; fr_q_sum = 0;
    }

    inline void fr_assign_true(int v) {
        if (!ckpt_enabled) return;
        for (uint32_t k = ck_head_off[v]; k < ck_head_off[v+1]; k++) {
            uint32_t cl = ck_head_cl[k];
            ck_head_true[cl] = 1;
            if (ck_ntc[cl] == 0) frontier_open++;
        }
        for (uint32_t k = ck_cause_off[v]; k < ck_cause_off[v+1]; k++) {
            uint32_t cl = ck_cause_cl[k];
            if (ck_ntc[cl]++ == 0 && ck_head_true[cl]) frontier_open--;
        }
    }
    inline void fr_unassign_true(int v) {
        if (!ckpt_enabled) return;
        for (uint32_t k = ck_head_off[v]; k < ck_head_off[v+1]; k++) {
            uint32_t cl = ck_head_cl[k];
            ck_head_true[cl] = 0;
            if (ck_ntc[cl] == 0) frontier_open--;
        }
        for (uint32_t k = ck_cause_off[v]; k < ck_cause_off[v+1]; k++) {
            uint32_t cl = ck_cause_cl[k];
            if (--ck_ntc[cl] == 0 && ck_head_true[cl]) frontier_open++;
        }
    }


    // In-place compaction of the clause arena. Clause ORDER is preserved,
    // so problem clauses keep their ids (0..n_problem_clauses-1) and the
    // search trajectory is bit-for-bit unchanged: propagation already
    // skipped removed clauses, watch-list order of live entries is kept,
    // and reasons are remapped to the moved ids.
    void garbage_collect() {
        int nc = cl_count();
        vector<int32_t> cid_map(nc, -1);

        size_t wlit = 0;
        int    wcid = 0;
        for (int c = 0; c < nc; c++) {
            if (removed[c]) continue;
            uint32_t b  = cl_begin[c];
            uint32_t sz = cl_size[c];
            if (wlit != b)
                memmove(&lit_arena[wlit], &lit_arena[b], sz * sizeof(int32_t));
            cid_map[c]    = wcid;
            cl_begin[wcid] = (uint32_t)wlit;
            cl_size [wcid] = sz;
            lbd     [wcid] = lbd[c];
            removed [wcid] = 0;
            wlit += sz;
            wcid++;
        }
        lit_arena.resize(wlit);
        cl_begin.resize(wcid);
        cl_size .resize(wcid);
        lbd     .resize(wcid);
        removed .resize(wcid);

        // Remap watches: drop stale entries (removed clauses), remap live
        // long-clause cids; binary entries (BIN_CID) are untouched.
        for (auto& wl : watches) {
            size_t w = 0;
            for (size_t r = 0; r < wl.size(); r++) {
                Watch& x = wl[r];
                if (x.cid >= 0) {
                    int m = cid_map[x.cid];
                    if (m < 0) continue;          // clause gone: drop watch
                    wl[w++] = {m, x.blocker};
                } else {
                    wl[w++] = x;                  // binary
                }
            }
            wl.resize(w);
        }

        // Remap reasons (locked clauses are never removed, so map >= 0).
        for (int v = 1; v <= num_vars; v++)
            if (reason[v] >= 0) reason[v] = cid_map[reason[v]];

        // Actually give memory back when the slack is large.
        if (lit_arena.capacity() > 2 * lit_arena.size()) lit_arena.shrink_to_fit();

        arena_wasted = 0;
        n_gc++;
    }

    void backtrack_to(int btlevel) {
        if (decision_level() <= btlevel) return;
        int target = trail_lim[btlevel];
        for (int i = (int)trail.size() - 1; i >= target; i--) {
            int v = trail[i];

            phase[v] = assignment[v];
            if (assignment[v] == 1) fr_unassign_true(v);
            assignment[v] = 0;
            level[v] = -1;
            reason[v] = -1;
            order_heap.insert(v);
        }
        trail.resize(target);
        trail_lim.resize(btlevel);
        qhead = target;
    }

    static double luby(double y, int x) {

        int size, seq;
        for (size = 1, seq = 0; size < x + 1; seq++, size = size*2 + 1);
        while (size - 1 != x) {
            size = (size - 1) >> 1;
            seq--;
            x = x % size;
        }
        return pow(y, seq);
    }

    int pick_branch_var() {
        while (!order_heap.empty()) {
            int v = order_heap.extract_max();
            if (assignment[v] == 0) return v;
        }
        return -1;
    }

    long long n_flp_units = 0;
    long long n_flp_probes = 0;
    long long n_flp_sibling_skips = 0;
    int        flp_no_unit_streak_cap = 200;

    bool failed_literal_probing(int max_rounds = 3) {

        const int    FLP_MIN_CLAUSES   = 10000;
        const double FLP_MIN_BIN_RATIO = 0.85;
        double bin_ratio = (double)n_binary_clauses / max(1LL, n_clauses_added);
        if (n_clauses_added < FLP_MIN_CLAUSES)  return true;
        if (bin_ratio < FLP_MIN_BIN_RATIO)      return true;

        vector<int> degree(num_vars + 1, 0);
        for (int cid = 0; cid < n_problem_clauses; cid++) {
            int32_t* cl = cl_data(cid);
            int sz = (int)cl_len(cid);
            for (int kk = 0; kk < sz; kk++) degree[var_of(cl[kk])]++;
        }
        // binaries live in the watch lists; each binary contributes one
        // watch entry per literal, so this counts them exactly once per side
        for (int li = 0; li < (int)watches.size(); li++) {
            const auto& wl = watches[li];
            for (const Watch& w : wl)
                if (w.cid == BIN_CID) degree[var_of(li)]++;
        }
        vector<int> all_vars_by_degree;
        all_vars_by_degree.reserve(num_vars);
        for (int v = 1; v <= num_vars; v++) all_vars_by_degree.push_back(v);
        sort(all_vars_by_degree.begin(), all_vars_by_degree.end(),
             [&](int a, int b){ return degree[a] > degree[b]; });

        vector<uint8_t> skip_pos_probe;
        if (planning_pattern_detected) {
            skip_pos_probe.assign(num_vars + 1, 0);
        }

        for (int round = 0; round < max_rounds; round++) {
            long long units_this_round = 0;
            int no_unit_streak = 0;
            if (planning_pattern_detected) {

                std::fill(skip_pos_probe.begin(), skip_pos_probe.end(), 0);
            }

            for (int v : all_vars_by_degree) {
                if (assignment[v] != 0) continue;

                bool fail_pos = false, fail_neg = false;
                bool did_probe_pos = false;

                if (!planning_pattern_detected || !skip_pos_probe[v]) {
                    did_probe_pos = true;
                    int trail_size_before = (int)trail.size();
                    trail_lim.push_back(trail_size_before);
                    assignment[v] = 1;
                    level[v] = 1;
                    reason[v] = -1;
                    trail.push_back(v);
                    n_flp_probes++;
                    int confl = propagate();
                    if (confl != -1) fail_pos = true;
                    for (int i = (int)trail.size() - 1; i >= trail_size_before; i--) {
                        int u = trail[i];
                        assignment[u] = 0;
                        level[u] = -1;
                        reason[u] = -1;
                    }
                    trail.resize(trail_size_before);
                    trail_lim.pop_back();
                    qhead = trail_size_before;
                } else {
                    n_flp_sibling_skips++;
                }

                {
                    int trail_size_before = (int)trail.size();
                    trail_lim.push_back(trail_size_before);
                    assignment[v] = -1;
                    level[v] = 1;
                    reason[v] = -1;
                    trail.push_back(v);
                    n_flp_probes++;
                    int confl = propagate();
                    if (confl != -1) fail_neg = true;
                    for (int i = (int)trail.size() - 1; i >= trail_size_before; i--) {
                        int u = trail[i];
                        assignment[u] = 0;
                        level[u] = -1;
                        reason[u] = -1;
                    }
                    trail.resize(trail_size_before);
                    trail_lim.pop_back();
                    qhead = trail_size_before;
                }

                if (fail_pos && fail_neg) {
                    if (drat) { drat_unit((v << 1) | 1); drat_unit(v << 1); drat_empty(); }
                    return false;
                }

                if (fail_pos || fail_neg) {
                    int val = fail_pos ? -1 : 1;
                    drat_unit(fail_pos ? ((v << 1) | 1) : (v << 1));
                    assignment[v] = (int8_t)val;
                    level[v] = 0;
                    reason[v] = -2;
                    trail.push_back(v);
                    if (assignment[v] == 1) fr_assign_true(v);
                    n_flp_units++;
                    units_this_round++;
                    no_unit_streak = 0;
                    int confl = propagate();
                    if (confl != -1) { drat_empty(); return false; }
                } else {
                    no_unit_streak++;
                    if (no_unit_streak >= flp_no_unit_streak_cap) break;
                }

                if (planning_pattern_detected && did_probe_pos && fail_pos) {
                    const int* ss = sib_data(v);
                    int sn = sib_len(v);
                    for (int kk = 0; kk < sn; kk++) {
                        int s = ss[kk];
                        if (assignment[s] == 0) skip_pos_probe[s] = 1;
                    }
                }
            }

            if (units_this_round == 0) break;
        }
        return true;
    }

    int solve() {
        auto t0 = chrono::high_resolution_clock::now();

        int c0 = propagate();
        if (c0 != -1) {
            drat_empty();
            solve_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
            return 20;
        }

        if (!failed_literal_probing()) {
            solve_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
            return 20;
        }

        max_learnts = max(100LL, n_clauses_added / 3);

        adaptive_restart = (n_clauses_added >= adaptive_restart_gate);
        lbd_queue_clear();
        trail_q_n = 0; trail_q_i = 0; trail_q_sum = 0;
        lbd_global_sum = 0.0;

        long long restart_conflicts = (long long)(restart_base * luby(2.0, (int)n_restarts));
        long long conflicts_since_restart = 0;

        vector<int> learnt;             // reused across conflicts (no per-conflict alloc)

        while (true) {
            int conflict_cid = propagate();
            if (conflict_cid != -1) {
                n_conflicts++;
                conflicts_since_restart++;
                if (ckpt_enabled) fr_queue_push(frontier_open);
                if (decision_level() == 0) {
                    drat_empty();
                    solve_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
                    return 20;
                }

                if (adaptive_restart) {
                    // Trail-size blocking (Glucose): if the trail at conflict
                    // is much larger than recent average, the solver may be
                    // approaching a model — postpone restarts. Unlike stock
                    // Glucose (which waits 10000 conflicts), activate as soon
                    // as the trail queue has meaningful history: planning SAT
                    // instances often solve in <10K conflicts and need the
                    // protection from the start.
                    if (trail_q_n >= 100 && lbd_q_n == LBD_QUEUE_CAP &&
                        (double)trail.size() > restart_R * ((double)trail_q_sum / max(1, trail_q_n))) {
                        lbd_queue_clear();
                    }
                    trail_queue_push((int)trail.size());
                }

                int btlevel;
                analyze(conflict_cid, learnt, btlevel);
                backtrack_to(btlevel);

                if ((int)learnt.size() == 1) {
                    drat_unit(learnt[0]);

                    int li = learnt[0];
                    int v = var_of(li);
                    int val = is_pos(li) ? 1 : -1;
                    assignment[v] = (int8_t)val;
                    level[v] = 0;
                    reason[v] = -2;
                    trail.push_back(v);
                    if (assignment[v] == 1) fr_assign_true(v);
                    if (adaptive_restart) { lbd_queue_push(1); lbd_global_sum += 1.0; }
                } else if ((int)learnt.size() == 2) {
                    drat_bin(learnt[0], learnt[1]);
                    // Learnt binary: attach to the merged watch lists,
                    // assert learnt[0] with the encoded-literal reason.
                    watches[learnt[0]].push_back({BIN_CID, (int32_t)learnt[1]});
                    watches[learnt[1]].push_back({BIN_CID, (int32_t)learnt[0]});
                    n_learned++;
                    if (adaptive_restart) { lbd_queue_push(2); lbd_global_sum += 2.0; }

                    int li = learnt[0];
                    int v = var_of(li);
                    int val = is_pos(li) ? 1 : -1;
                    assignment[v] = (int8_t)val;
                    level[v] = btlevel;
                    reason[v] = enc_bin(learnt[1]);
                    trail.push_back(v);
                    if (assignment[v] == 1) fr_assign_true(v);
                } else {
                    drat_clause(learnt);
                    int learnt_lbd = compute_lbd(learnt);
                    int cid = add_learned_clause(learnt, learnt_lbd);
                    n_learned++;
                    if (adaptive_restart) { lbd_queue_push(learnt_lbd); lbd_global_sum += learnt_lbd; }

                    int li = learnt[0];
                    int v = var_of(li);
                    int val = is_pos(li) ? 1 : -1;
                    assignment[v] = (int8_t)val;
                    level[v] = btlevel;
                    reason[v] = cid;
                    trail.push_back(v);
                    if (assignment[v] == 1) fr_assign_true(v);
                }
            } else {

                bool do_restart;
                if (adaptive_restart) {
                    do_restart = (lbd_q_n == LBD_QUEUE_CAP) &&
                        ((double)lbd_q_sum / LBD_QUEUE_CAP) * restart_K >
                        (lbd_global_sum / (double)max(1LL, n_conflicts));
                } else {
                    do_restart = conflicts_since_restart >= restart_conflicts;
                }
                // Semantic restart blocking: the unexplained frontier is
                // shrinking -> the plan is closing -> keep going.
                if (do_restart && temporal_banded && !ckpt_built)
                    build_frontier_structs();
                if (do_restart && frontier_shrinking()) {
                    do_restart = false;
                    n_restart_blocks++;
                }
                if (do_restart) {
                    n_restarts++;
                    conflicts_since_restart = 0;
                    lbd_queue_clear();
                    restart_conflicts = (long long)(restart_base * luby(2.0, (int)n_restarts));
                    backtrack_to(0);
                    // satori-49: refresh forward/source priority so VSIDS decay
                    // does not erase it. Scaled by var_inc to stay proportional
                    // to current activity magnitude; sift-up only (safe).
                    if (s49_on && s49_kick > 0.0f && temporal_banded && !tprio.empty()) {
                        float base = (float)var_inc * s49_kick;
                        for (int v = 1; v <= num_vars; v++) {
                            if (assignment[v] == 0 && tprio[v] > 0.0f) {
                                activity[v] += base * tprio[v];
                                order_heap.increase(v);
                            }
                        }
                    }
                }

                if (decision_level() == 0 && n_learnts_alive > max_learnts) {
                    reduce_db();
                }

                int v = pick_branch_var();
                if (v == -1) {

                    solve_time = chrono::duration<double>(chrono::high_resolution_clock::now() - t0).count();
                    return 10;
                }
                int val = phase[v] >= 0 ? phase[v] : -1;
                if (val == 0) val = -1;
                trail_lim.push_back((int)trail.size());
                assignment[v] = (int8_t)val;
                level[v] = decision_level();
                reason[v] = -1;
                trail.push_back(v);
                n_decisions++;
                if (assignment[v] == 1) fr_assign_true(v);
            }
        }
    }

    bool verify() {
        auto lit_sat = [&](int mapped) {
            int v = var_of(mapped);
            int a = assignment[v];
            if (a == 0) a = 1;
            return is_pos(mapped) ? (a == 1) : (a == -1);
        };

        if (scc_applied) {
            int n = (int)verify_off.size() - 1;
            for (int i = 0; i < n; i++) {
                bool sat = false;
                for (uint32_t k = verify_off[i]; k < verify_off[i+1]; k++) {
                    if (lit_sat(lit_remap[verify_lits[k]])) { sat = true; break; }
                }
                if (!sat) return false;
            }
            return true;
        }

        for (int cid = 0; cid < n_problem_clauses; cid++) {
            int32_t* cl = cl_data(cid);
            int sz = (int)cl_len(cid);
            bool sat = false;
            for (int kk = 0; kk < sz; kk++) {
                if (lit_sat(cl[kk])) { sat = true; break; }
            }
            if (!sat) return false;
        }
        // Binary clauses live only in the watch lists; each appears once
        // per side. (Learnt binaries are checked too — harmless, since any
        // model of the formula satisfies its implied clauses.)
        for (int li = 0; li < (int)watches.size(); li++) {
            for (const Watch& w : watches[li]) {
                if (w.cid != BIN_CID) continue;
                if (!lit_sat(li) && !lit_sat(w.blocker)) return false;
            }
        }
        return true;
    }

    void run() {
        auto t_total = chrono::high_resolution_clock::now();
        bool ok = parse_cnf();
        int rc;
        if (!ok) rc = 20;
        else      rc = solve();
        double total = chrono::duration<double>(chrono::high_resolution_clock::now() - t_total).count();

        cout << "c ====================================================================" << endl;
        cout << "c SATori (clause-span + frontier-restarts + temporal-adaptive + deep-ccmin + 1-UIP + ccmin + VSIDS + merged watches + inline binaries)" << endl;
        cout << "c Input: " << cnf_file << endl;
        cout << "c Variables: " << num_vars << "  Clauses: " << num_clauses_input << endl;
        printf("c Parse Time: %.3f ms\n", parse_time * 1000);
        printf("c Solve Time: %.3f ms\n", solve_time * 1000);
        printf("c Total Time: %.3f ms\n", total      * 1000);
        cout << "c Decisions: "    << n_decisions    << endl;
        cout << "c Conflicts: "    << n_conflicts    << endl;
        cout << "c Propagations: " << n_propagations << endl;
        cout << "c FLP Probes: "   << n_flp_probes   << endl;
        cout << "c FLP Units: "    << n_flp_units    << endl;
        cout << "c FLP Sibling Skips: " << n_flp_sibling_skips << endl;
        cout << "c SCC Substituted Vars: " << n_scc_subst_vars << endl;
        cout << "c SCC Removed Binaries: " << n_scc_bin_removed << endl;
        cout << "c Planning Heads: " << n_heads << endl;
        cout << "c Planning Sibling Pairs: " << n_sibling_pairs << endl;
        cout << "c Frontier Restart Blocks: " << n_restart_blocks << endl;
        cout << "c Temporal Band: " << (temporal_banded ? "yes" : "no") << "  (p90 gap " << band_p90 << " / " << num_vars << " vars, mutex frac " << mutex_frac << ", ramp " << (temporal_banded ? (mutex_frac >= 0.70 ? "center" : "forward") : "-") << ")" << endl;
        cout << "c Planning Pattern Detected: " << (planning_pattern_detected ? "yes" : "no") << endl;
        cout << "c Learned: "      << n_learned      << endl;
        cout << "c Learnts Alive: " << n_learnts_alive << endl;
        cout << "c DB Reductions: " << n_reductions << "  (arena GC: " << n_gc << ")" << endl;
        cout << "c Restarts: "     << n_restarts     << endl;
        cout << "c Restart Strategy: " << (adaptive_restart ? "lbd-adaptive" : "luby") << endl;
        if (rc == 10) {
            bool v = verify();
            cout << "s SATISFIABLE" << endl;
            cout << "c Valid: " << (v ? "True" : "False") << endl;
        } else {
            cout << "s UNSATISFIABLE" << endl;
        }
    }
};

int main(int argc, char** argv) {
    if (argc < 2) { cerr << "Usage: " << argv[0] << " <file.cnf> [proof.drat]" << endl; return 1; }
    SatoriCDCL s;
    s.cnf_file = argv[1];
    if (argc >= 3) {
        s.drat = fopen(argv[2], "w");
        if (!s.drat) { cerr << "ERROR: cannot open proof file " << argv[2] << endl; return 1; }
    }
    s.run();
    if (s.drat) fclose(s.drat);
    return 0;
}