Answer

Fix: Canonical ROBDD with hash‑consed unique/computed tables, exact BigInt model counting, and reachability fixpoint for js-robdd-canonical-apply-restrict-model-count-fixpoint-exactness

The full artifact is saved at /workspace/solution.md (source modules at ~/robdd/). Below is the self‑contained solution.

1. Root‑cause analysis

Failing implementations of this class hit one of five defects:

1. Non‑canonical representation. mk(var, low, high) must (a) return low when low === high (reduction), and (b) key surviving nodes by (var, low, high) in a unique table. Missing either makes logically equivalent formulas map to different ids.
2. Variable order not fixed/ respected. Node ids are canonical only relative to one order. Store var as a rank (0 = top); apply splits on min(rank(a), rank(b)); mk is only called with a rank smaller than its children's.
3. Wrong fixpoint semantics. Reachability is the least fixpoint R₀ = I, R₊ = R ∪ ∃s.(R(s) ∧ T(s,s')), with next‑state vars renamed back via real substitution (compose(yᵢ, xᵢ)), iterated to stability. Invariant P holds iff R ∧ ¬P ≡ FALSE.
4. compose breaking order. A structural compose(a,v,f) can splice f (which may mention a lower rank than v) under a rank‑v node. The fix uses the order‑preserving identity compose(a,v,f) = (a|v=0 ∧ ¬f) ∨ (a|v=1 ∧ f) built only from restrict/apply.
5. Model count losing don't‑care paths / using Number. Counting must be BigInt and must multiply by 2^(skipped counted levels) when a node's top rank is deeper than the next counted rank.

2. Exact fix

robdd.js

'use strict';

/**
 * Reduced Ordered Binary Decision Diagram (ROBDD) manager.
 *
 * Design
 * ------
 * - Two terminal nodes are preallocated:  0 = FALSE, 1 = TRUE.
 * - An internal node is the triple (var, low, high) where `var` is the
 *   *rank* of the decision variable (0 is the root-most / smallest rank).
 * - The *unique table* hash-conses every node: two calls to `mk(v, lo, hi)`
 *   with the same triple return the same integer id.  Combined with the
 *   reduction rule `mk(v, x, x) === x` this yields a canonical
 *   representation.
 * - The *computed table* caches every binary apply / restrict / not result.
 * - `satCount` returns a BigInt and accounts for skipped ("don't-care")
 *   levels by multiplying by 2^(number of skipped counted variables).
 */

const FALSE = 0;
const TRUE = 1;

const COMMUTATIVE = new Set(['and', 'or', 'xor', 'nand', 'nor', 'xnor']);

class BDDManager {
  constructor(varOrder) {
    this._order = [];
    this._rank = new Map();
    this._autoOrder = false;

    if (Array.isArray(varOrder)) {
      varOrder.forEach((name) => this._addVar(name));
    } else if (varOrder && typeof varOrder === 'object') {
      const entries = Object.keys(varOrder).map((name) => [name, varOrder[name]]);
      entries.sort((a, b) => a[1] - b[1]);
      entries.forEach(([name]) => this._addVar(name));
    } else {
      this._autoOrder = true;
    }

    this.nodes = [
      { id: FALSE, var: Infinity, low: null, high: null, terminal: 0 },
      { id: TRUE, var: Infinity, low: null, high: null, terminal: 1 },
    ];
    this.unique = new Map(); // "var,low,high" -> id
    this.cache = new Map();  // computed table
    this._nextId = 2;
  }

  _addVar(name) {
    if (this._rank.has(name)) return this._rank.get(name);
    const rank = this._order.length;
    this._order.push(name);
    this._rank.set(name, rank);
    return rank;
  }

  rank(name) {
    if (this._rank.has(name)) return this._rank.get(name);
    if (!this._autoOrder) throw new Error(`Unknown variable "${name}" for a fixed variable order`);
    return this._addVar(name);
  }

  varName(rank) { return this._order[rank]; }
  get numVars() { return this._order.length; }

  lit(name, positive = true) {
    const v = this.rank(name);
    const node = this.mk(v, FALSE, TRUE);
    return positive ? node : this.not(node);
  }
  variable(name) { return this.lit(name, true); }

  ithVar(i) {
    while (this._order.length <= i && this._autoOrder) this._addVar('v' + this._order.length);
    if (i >= this._order.length) throw new Error(`No variable at rank ${i}`);
    return this.mk(i, FALSE, TRUE);
  }
  nthVar(i) { return this.ithVar(i); }
  getVarName(i) { return this._order[i]; }

  setVariableOrder(order) {
    if (this.nodes.length > 2) throw new Error('Variable order must be set before any nodes are built');
    this._order = [];
    this._rank = new Map();
    this._autoOrder = false;
    order.forEach((name) => this._addVar(name));
  }
  uniqueSize() { return this.unique.size; }

  mk(v, low, high) {
    if (low === high) return low; // reduction rule
    const key = v + ',' + low + ',' + high;
    const hit = this.unique.get(key);
    if (hit !== undefined) return hit;
    const id = this._nextId++;
    this.nodes[id] = { id, var: v, low, high };
    this.unique.set(key, id);
    return id;
  }

  get false() { return FALSE; }
  get true() { return TRUE; }

  apply(op, a, b) {
    if (op === 'not') return this.not(a);
    if (op === 'nand') return this.not(this.apply('and', a, b));
    if (op === 'nor') return this.not(this.apply('or', a, b));
    if (op === 'xnor') return this.not(this.apply('xor', a, b));

    switch (op) {
      case 'and':
        if (a === FALSE || b === FALSE) return FALSE;
        if (a === TRUE) return b;
        if (b === TRUE) return a;
        if (a === b) return a;
        break;
      case 'or':
        if (a === TRUE || b === TRUE) return TRUE;
        if (a === FALSE) return b;
        if (b === FALSE) return a;
        if (a === b) return a;
        break;
      case 'xor':
        if (a === FALSE) return b;
        if (b === FALSE) return a;
        if (a === TRUE) return this.not(b);
        if (b === TRUE) return this.not(a);
        if (a === b) return FALSE;
        break;
      case 'imp':
        if (a === FALSE || b === TRUE) return TRUE;
        if (a === TRUE) return b;
        if (b === FALSE) return this.not(a);
        if (a === b) return TRUE;
        break;
      default:
        throw new Error(`Unsupported op "${op}"`);
    }

    let ka = a, kb = b;
    if (COMMUTATIVE.has(op) && ka > kb) { const t = ka; ka = kb; kb = t; }
    const ckey = op + ':' + ka + ':' + kb;
    const cached = this.cache.get(ckey);
    if (cached !== undefined) return cached;

    const va = this.nodes[a].var;
    const vb = this.nodes[b].var;
    const v = va < vb ? va : vb;

    let al, ah, bl, bh;
    if (va === v) { al = this.nodes[a].low; ah = this.nodes[a].high; } else { al = ah = a; }
    if (vb === v) { bl = this.nodes[b].low; bh = this.nodes[b].high; } else { bl = bh = b; }

    const lo = this.apply(op, al, bl);
    const hi = this.apply(op, ah, bh);
    const r = this.mk(v, lo, hi);
    this.cache.set(ckey, r);
    return r;
  }

  not(a) {
    if (a === FALSE) return TRUE;
    if (a === TRUE) return FALSE;
    const key = 'not:' + a;
    const cached = this.cache.get(key);
    if (cached !== undefined) return cached;
    const n = this.nodes[a];
    const r = this.mk(n.var, this.not(n.low), this.not(n.high));
    this.cache.set(key, r);
    return r;
  }
  negate(a) { return this.not(a); }

  and(a, b) { return this.apply('and', a, b); }
  or(a, b)  { return this.apply('or', a, b); }
  xor(a, b) { return this.apply('xor', a, b); }
  imp(a, b) { return this.apply('imp', a, b); }
  nand(a, b){ return this.apply('nand', a, b); }
  nor(a, b) { return this.apply('nor', a, b); }
  xnor(a, b){ return this.apply('xnor', a, b); }

  ite(f, g, h) { return this.or(this.and(f, g), this.and(this.not(f), h)); }

  restrict(a, nameOrRank, value) {
    const v = typeof nameOrRank === 'number' ? nameOrRank : this.rank(nameOrRank);
    return this._restrict(a, v, value ? 1 : 0);
  }

  _restrict(a, v, bit) {
    if (a === FALSE || a === TRUE) return a;
    const av = this.nodes[a].var;
    if (av === v) return bit ? this.nodes[a].high : this.nodes[a].low;
    if (av > v) return a;
    const key = 'restrict:' + a + ':' + v + ':' + bit;
    const cached = this.cache.get(key);
    if (cached !== undefined) return cached;
    const n = this.nodes[a];
    const r = this.mk(n.var, this._restrict(n.low, v, bit), this._restrict(n.high, v, bit));
    this.cache.set(key, r);
    return r;
  }

  compose(a, nameOrRank, f) {
    const v = typeof nameOrRank === 'number' ? nameOrRank : this.rank(nameOrRank);
    const key = 'compose:' + a + ':' + v + ':' + f;
    const cached = this.cache.get(key);
    if (cached !== undefined) return cached;
    const cof0 = this._restrict(a, v, 0);
    const cof1 = this._restrict(a, v, 1);
    const nf = this.not(f);
    const r = this.or(this.and(nf, cof0), this.and(f, cof1));
    this.cache.set(key, r);
    return r;
  }

  composeAll(a, substitutions) {
    let r = a;
    for (const [name, f] of substitutions) r = this.compose(r, name, f);
    return r;
  }

  existsVar(a, nameOrRank) {
    const v = typeof nameOrRank === 'number' ? nameOrRank : this.rank(nameOrRank);
    const key = 'exists:' + a + ':' + v;
    const cached = this.cache.get(key);
    if (cached !== undefined) return cached;
    const r = this.or(this._restrict(a, v, 0), this._restrict(a, v, 1));
    this.cache.set(key, r);
    return r;
  }
  exists(a, vars) { let r = a; for (const v of vars) r = this.existsVar(r, v); return r; }

  forallVar(a, nameOrRank) {
    const v = typeof nameOrRank === 'number' ? nameOrRank : this.rank(nameOrRank);
    const key = 'forall:' + a + ':' + v;
    const cached = this.cache.get(key);
    if (cached !== undefined) return cached;
    const r = this.and(this._restrict(a, v, 0), this._restrict(a, v, 1));
    this.cache.set(key, r);
    return r;
  }
  forall(a, vars) { let r = a; for (const v of vars) r = this.forallVar(r, v); return r; }

  satCount(a, vars) {
    const levels = (vars === undefined
      ? this._order.map((_, i) => i)
      : vars.map((v) => (typeof v === 'number' ? v : this.rank(v)))
    ).slice().sort((x, y) => x - y);

    const memo = new Map();
    const n = levels.length;

    const firstAtLeast = (v, start) => {
      let lo = start, hi = n;
      while (lo < hi) {
        const mid = (lo + hi) >> 1;
        if (levels[mid] < v) lo = mid + 1; else hi = mid;
      }
      return lo;
    };

    const rec = (id, i) => {
      if (id === FALSE) return 0n;
      if (id === TRUE) return 1n << BigInt(n - i);
      const mkey = id * (n + 1) + i;
      const hit = memo.get(mkey);
      if (hit !== undefined) return hit;

      const v = this.nodes[id].var;
      const j = firstAtLeast(v, i);
      if (j >= n || levels[j] !== v) {
        throw new Error(`satCount: node ${id} depends on var rank ${v} which is not in the counted set`);
      }
      const free = j - i;
      const sub = rec(this.nodes[id].low, j + 1) + rec(this.nodes[id].high, j + 1);
      const r = sub << BigInt(free);
      memo.set(mkey, r);
      return r;
    };

    return rec(a, 0);
  }

  modelCount(a) { return this.satCount(a); }

  nodeCount(a, seen = new Set()) {
    if (a === FALSE || a === TRUE || seen.has(a)) return seen.size;
    seen.add(a);
    const nd = this.nodes[a];
    this.nodeCount(nd.low, seen);
    this.nodeCount(nd.high, seen);
    return seen.size;
  }

  get uniqueTableSize() { return this.unique.size; }
  get computedTableSize() { return this.cache.size; }
  clearCache() { this.cache.clear(); }

  serialize(a) {
    const remap = new Map([[FALSE, 0], [TRUE, 1]]);
    const out = [];
    let next = 2;
    const visit = (id) => {
      if (remap.has(id)) return remap.get(id);
      const nd = this.nodes[id];
      const lo = visit(nd.low);
      const hi = visit(nd.high);
      const stable = next++;
      remap.set(id, stable);
      out.push({ id: stable, var: nd.var, name: this._order[nd.var], low: lo, high: hi });
      return stable;
    };
    const rootStable = visit(a);
    out.sort((x, y) => x.id - y.id);
    return { root: rootStable, nodes: out };
  }

  toString(a) {
    const nameOf = (v) => (v === Infinity ? '#' : (this._order[v] ?? 'v' + v));
    const rec = (id) => {
      if (id === FALSE) return 'F';
      if (id === TRUE) return 'T';
      const nd = this.nodes[id];
      return `(${nameOf(nd.var)} ${rec(nd.low)} ${rec(nd.high)})`;
    };
    return rec(a);
  }
}

module.exports = { BDDManager, FALSE, TRUE };

modelcheck.js

'use strict';

const { BDDManager, FALSE } = require('./robdd');

function buildTransitionRelation(mgr, stateVars, nextVars, nextFns) {
  let t = mgr.true;
  for (let i = 0; i < stateVars.length; i++) {
    const sv = mgr.variable(stateVars[i]);
    const nv = mgr.variable(nextVars[i]);
    const f = nextFns[stateVars[i]];
    if (f === undefined) throw new Error(`Missing next-state function for ${stateVars[i]}`);
    const bit = mgr.xnor(nv, f); // next_i <-> f
    t = mgr.and(t, bit);
  }
  return t;
}

function image(mgr, R, trans, stateVars, nextVars) {
  let img = mgr.and(R, trans);
  img = mgr.exists(img, stateVars);
  for (let i = 0; i < nextVars.length; i++) {
    img = mgr.compose(img, nextVars[i], mgr.variable(stateVars[i]));
  }
  return img;
}

function reachableFixpoint(mgr, { init, trans, stateVars, nextVars, invariant }) {
  let R = init;
  const iterationCounts = [mgr.satCount(R, stateVars)];

  while (true) {
    const img = image(mgr, R, trans, stateVars, nextVars);
    const Rnext = mgr.or(R, img);
    if (Rnext === R) break;
    R = Rnext;
    iterationCounts.push(mgr.satCount(R, stateVars));
  }

  let invariantHolds = true;
  if (invariant !== undefined) {
    const bad = mgr.and(R, mgr.not(invariant));
    invariantHolds = bad === FALSE;
  }

  return {
    reachable: R,
    iterationCounts,
    invariantHolds,
    finalCount: mgr.satCount(R, stateVars),
    iterations: iterationCounts.length,
  };
}

module.exports = { buildTransitionRelation, image, reachableFixpoint, BDDManager };

3. Verification

test.js cross‑checks every requirement, including a 200‑trial brute‑force comparison against truth tables.

'use strict';

const assert = require('assert');
const { BDDManager, FALSE, TRUE } = require('./robdd');
const { buildTransitionRelation, reachableFixpoint } = require('./modelcheck');

let passed = 0;
function check(name, fn) {
  try { fn(); console.log('PASS', name); passed++; }
  catch (e) { console.log('FAIL', name, '-', e.message); process.exitCode = 1; }
}

check('canonicity: idempotence and distributivity', () => {
  const m = new BDDManager(['a', 'b', 'c']);
  const a = m.variable('a'), b = m.variable('b'), c = m.variable('c');
  const f1 = m.or(m.and(a, b), m.and(a, c));
  const f2 = m.and(a, m.or(b, c));
  assert.strictEqual(f1, f2, 'distributivity must yield identical node ids');
  assert.strictEqual(m.and(a, a), a, 'a AND a === a');
  assert.strictEqual(m.not(m.not(a)), a, 'NOT NOT a === a');
  assert.strictEqual(m.xor(a, b), m.not(m.xnor(a, b)), 'xor === not(xnor)');
});

check('canonicity is independent of construction history', () => {
  const build = () => {
    const m = new BDDManager(['a', 'b', 'c', 'd']);
    const f = m.or(m.and(m.variable('a'), m.variable('b')), m.and(m.variable('c'), m.variable('d')));
    return { m, f };
  };
  const buildViaXor = () => {
    const m = new BDDManager(['a', 'b', 'c', 'd']);
    const f = m.or(m.and(m.variable('c'), m.variable('d')), m.and(m.variable('a'), m.variable('b')));
    return { m, f };
  };
  const p = build(), q = buildViaXor();
  assert.deepStrictEqual(p.m.serialize(p.f), q.m.serialize(q.f));
});

check('unique table size and stable serialised ids', () => {
  const m = new BDDManager(['a', 'b', 'c']);
  const a = m.variable('a'), b = m.variable('b');
  const f = m.and(a, b);
  assert.strictEqual(m.uniqueTableSize, 3, 'unique table has exactly 3 internal nodes');
  const ser = m.serialize(f);
  assert.strictEqual(ser.root, 3, 'root serialises to stable id 3');
  assert.deepStrictEqual(ser.nodes, [
    { id: 2, var: 1, name: 'b', low: 0, high: 1 },
    { id: 3, var: 0, name: 'a', low: 0, high: 2 },
  ]);
  const r = m.restrict(f, 'b', 1);
  assert.strictEqual(r, a);
  assert.strictEqual(m.serialize(r).root, 2);
  const c = m.variable('c');
  const comp = m.compose(f, 'a', c);
  assert.strictEqual(comp, m.and(c, b));
});

check('satCount handles don\'t-care (skipped) levels', () => {
  const m = new BDDManager(['a', 'b', 'c']);
  const a = m.variable('a');
  assert.strictEqual(m.satCount(a, ['a']), 1n);
  assert.strictEqual(m.satCount(a, ['a', 'b']), 2n);
  assert.strictEqual(m.satCount(a, ['a', 'b', 'c']), 4n);
  assert.strictEqual(m.modelCount(a), 4n);
});

check('satCount is exact for 20 variables (node20)', () => {
  const names = Array.from({ length: 20 }, (_, i) => 'v' + i);
  const m = new BDDManager(names);
  let all = m.true, any = m.false;
  for (const n of names) { all = m.and(all, m.variable(n)); any = m.or(any, m.variable(n)); }
  assert.strictEqual(m.satCount(all, names), 1n);
  assert.strictEqual(m.satCount(any, names), (1n << 20n) - 1n);
  assert.strictEqual(m.satCount(m.false, names), 0n);
  assert.strictEqual(m.satCount(m.true, names), 1n << 20n);
});

check('reachability fixpoint: exact per-iteration counts and invariant', () => {
  const N = 10;
  const stateVars = Array.from({ length: N }, (_, i) => 'x' + i);
  const nextVars = Array.from({ length: N }, (_, i) => 'y' + i);
  const m = new BDDManager([...stateVars, ...nextVars]);
  const x = stateVars.map((n) => m.variable(n));
  const y = nextVars.map((n) => m.variable(n));

  let init = m.true;
  for (let i = 0; i < N; i++) init = m.and(init, m.not(x[i]));

  let trans = m.false;
  let stay = m.true;
  for (let i = 0; i < N; i++) stay = m.and(stay, m.xnor(y[i], x[i]));
  trans = m.or(trans, stay);
  for (let i = 0; i < N; i++) {
    let term = m.true;
    for (let j = 0; j < N; j++) {
      const expected = j === i ? m.not(x[j]) : x[j];
      term = m.and(term, m.xnor(y[j], expected));
    }
    trans = m.or(trans, term);
  }

  const res = reachableFixpoint(m, { init, trans, stateVars, nextVars, invariant: m.true });
  const binomial = [1, 10, 45, 120, 210, 252, 210, 120, 45, 10, 1];
  const expected = []; let acc = 0n;
  for (let k = 0; k <= N; k++) { acc += BigInt(binomial[k]); expected.push(acc); }
  assert.deepStrictEqual(res.iterationCounts, expected);
  assert.strictEqual(res.finalCount, 1024n);
  assert.strictEqual(res.invariantHolds, true);

  let notZero = m.false;
  for (let i = 0; i < N; i++) notZero = m.or(notZero, x[i]);
  const res2 = reachableFixpoint(m, { init, trans, stateVars, nextVars, invariant: notZero });
  assert.strictEqual(res2.invariantHolds, false);
});

check('buildTransitionRelation + fixpoint on a 3-bit counter', () => {
  const stateVars = ['x0', 'x1', 'x2'];
  const nextVars = ['y0', 'y1', 'y2'];
  const m = new BDDManager([...stateVars, ...nextVars]);
  const x = stateVars.map((n) => m.variable(n));
  const nextFns = {};
  let carry = m.true;
  for (let i = 0; i < 3; i++) { nextFns[stateVars[i]] = m.xor(x[i], carry); carry = m.and(x[i], carry); }
  const trans = buildTransitionRelation(m, stateVars, nextVars, nextFns);
  let init = m.true;
  for (let i = 0; i < 3; i++) init = m.and(init, m.not(x[i]));
  const res = reachableFixpoint(m, { init, trans, stateVars, nextVars, invariant: m.true });
  assert.deepStrictEqual(res.iterationCounts, [1n, 2n, 3n, 4n, 5n, 6n, 7n, 8n]);
  assert.strictEqual(res.finalCount, 8n);
});

function fromTruthTable(m, n, table) {
  const build = (v, prefix) => {
    if (v === n) return table[prefix] ? TRUE : FALSE;
    const lo = build(v + 1, prefix << 1);
    const hi = build(v + 1, (prefix << 1) | 1);
    return m.mk(v, lo, hi);
  };
  return build(0, 0);
}

check('brute force: apply/satCount match truth tables for 5 variables', () => {
  const n = 5, size = 1 << n;
  const m = new BDDManager(Array.from({ length: n }, (_, i) => 'v' + i));
  let seed = 123456789;
  const rnd = () => { seed = (seed * 1103515245 + 12345) & 0x7fffffff; return seed; };
  for (let trial = 0; trial < 200; trial++) {
    const t1 = new Array(size).fill(0), t2 = new Array(size).fill(0);
    for (let i = 0; i < size; i++) { t1[i] = rnd() & 1; t2[i] = rnd() & 1; }
    const f1 = fromTruthTable(m, n, t1), f2 = fromTruthTable(m, n, t2);
    let w1 = 0; for (let i = 0; i < size; i++) w1 += t1[i];
    assert.strictEqual(m.satCount(f1), BigInt(w1));
    assert.strictEqual(m.and(f1, f2), fromTruthTable(m, n, t1.map((x, i) => x & t2[i])));
    assert.strictEqual(m.or(f1, f2),  fromTruthTable(m, n, t1.map((x, i) => x | t2[i])));
    assert.strictEqual(m.xor(f1, f2), fromTruthTable(m, n, t1.map((x, i) => x ^ t2[i])));
    assert.strictEqual(m.not(f1),     fromTruthTable(m, n, t1.map((x) => 1 - x)));
  }
});

check('compose with replacement using lower and higher rank variables', () => {
  const m = new BDDManager(['x0', 'x1', 'x2']);
  const x0 = m.variable('x0'), x1 = m.variable('x1'), x2 = m.variable('x2');
  assert.strictEqual(m.compose(m.and(x0, x1), 'x0', x2), m.and(x1, x2));
  assert.strictEqual(m.compose(m.or(x2, x1), 'x2', x0), m.or(x0, x1));
  assert.strictEqual(m.compose(m.or(x0, x1), 'x0', m.and(x1, x2)), m.or(x1, m.and(x1, x2)));
});

console.log(`\n${passed} checks passed`);

Observed output

$ node test.js
PASS canonicity: idempotence and distributivity
PASS canonicity is independent of construction history
PASS unique table size and stable serialised ids
PASS satCount handles don't-care (skipped) levels
PASS satCount is exact for 20 variables (node20)
PASS reachability fixpoint: exact per-iteration counts and invariant
PASS buildTransitionRelation + fixpoint on a 3-bit counter
PASS brute force: apply/satCount match truth tables for 5 variables
PASS compose with replacement using lower and higher rank variables

9 checks passed

Key exact values asserted

Check	Expected	Meaning
unique table for a ∧ b	3	nodes a, b, a∧b
serialize(a ∧ b).root	3	stable post‑order id
serialize(a ∧ b).nodes	[(2,b,F,T),(3,a,F,2)]	canonical dump
restrict(a∧b, b, 1)	a, stable id 2	cofactor
compose(a∧b, a, c)	c ∧ b (same id)	substitution
satCount(a, [a,b,c])	4n	don't‑care factor 2²
satCount(∧v₀..v₁₉, all)	1n	node20 conjunct
satCount(∨v₀..v₁₉, all)	1048575n	node20 disjunct
10‑bit flip reachable counts	1,11,56,176,386,638,848,968,1013,1023,1024	cumulative binomials
final reachable count	1024n	all 2¹⁰ states

Reproduce

node test.js

# Evidence
- Problem class: js-robdd-canonical-apply-restrict-model-count-fixpoint-exactness
- Model: openrouter/deepseek/deepseek-v4.1-flash
- Solved: 2026-10-02T04:10:49.460Z
- Verification: solution produced by pi in sandbox; see signatures.json

{"description": "Implement a Reduced Ordered Binary Decision Diagram package in JavaScript with hash-consed unique and computed tables, then use it for symbolic model checking: encode a transition relation, iterate the existential-preimage reachable-state fixpoint, and check an invariant. The representation must be canonical under the supplied variable permutation, so logically equivalent formulas yield identical node ids, and the model count must be returned exactly as a BigInt with care for don't-care paths. Tests assert unique-table sizes, exact serialized node ids after apply/restrict/not/compose sequences, per-iteration reachable-state counts, and the final model count on node20.", "environment": "node20", "language": "js", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "js-robdd-canonical-apply-restrict-model-count-fixpoint-exactness", "provider": "openrouter", "solved_at": "2026-10-02T04:10:49.461Z", "version": "20"}