{"challengeId":"sat-shrink","entry":"verifier.mjs","sha256":"7f40629615aaaf4cf5dd91ecd923aa8e647109cb729556239cd7912cadd4fe9b","scoreDirection":"minimize","scoreLabel":"clauses","seedPolicy":{"mode":"fixed","testCount":1},"source":"// Frozen verifier for sat-shrink. It never runs solver code from the candidate.\n// A candidate returns pure data: { core: number[] }. We then brute-force every\n// Boolean assignment to prove the selected clauses are still UNSAT.\n\nconst VARS = 6;\n\n// Literals use DIMACS shape: positive n = x_n, negative n = !x_n.\n// Clauses 0..7 encode a compact parity-style contradiction over x1/x2/x3:\n// they require x1 xor x2 xor x3 to be both true and false. The rest are\n// satisfiable distractors that make the baseline bloated.\nconst CLAUSES = [\n  [1, 2, 3],\n  [1, -2, -3],\n  [-1, 2, -3],\n  [-1, -2, 3],\n  [-1, -2, -3],\n  [-1, 2, 3],\n  [1, -2, 3],\n  [1, 2, -3],\n  [4, 5],\n  [-4, 6],\n  [-5, -6],\n  [2, 4, -6],\n  [-2, 5],\n  [3, -4, 6],\n  [-3, -5],\n  [1, 4, 5],\n  [-1, -4, 6],\n  [2, -5, -6],\n];\n\nfunction gate(name, pass, detail) {\n  return { name, pass, detail };\n}\n\nfunction bad(name, detail) {\n  return { ok: false, score: null, gates: [gate(name, false, detail)], behavior: {}, logs: [] };\n}\n\nfunction litValue(lit, mask) {\n  const v = Math.abs(lit);\n  const bit = (mask >> (v - 1)) & 1;\n  return lit > 0 ? bit === 1 : bit === 0;\n}\n\nfunction clauseSat(clause, mask) {\n  return clause.some((lit) => litValue(lit, mask));\n}\n\nexport function verify(ctx) {\n  const sol = ctx.solution;\n  const core = sol && typeof sol === 'object' ? sol.core : undefined;\n  if (!Array.isArray(core)) return bad('structure', 'expected { core: number[] }');\n  if (core.length === 0) return bad('structure', 'core is empty');\n  if (core.length > CLAUSES.length) return bad('structure', `core has ${core.length} ids; formula has ${CLAUSES.length}`);\n\n  const seen = new Set();\n  let maxWidth = 0;\n  const selected = [];\n  for (const id of core) {\n    if (!Number.isInteger(id)) return bad('structure', `clause id ${String(id)} is not an integer`);\n    if (id < 0 || id >= CLAUSES.length) return bad('structure', `clause id ${id} is out of range`);\n    if (seen.has(id)) return bad('structure', `clause id ${id} appears twice`);\n    seen.add(id);\n    const clause = CLAUSES[id];\n    selected.push(clause);\n    if (clause.length > maxWidth) maxWidth = clause.length;\n  }\n\n  let witness = null;\n  for (let mask = 0; mask < 1 << VARS; mask++) {\n    if (selected.every((clause) => clauseSat(clause, mask))) {\n      witness = mask;\n      break;\n    }\n  }\n\n  const gates = [\n    gate('well-formed-core', true, `${core.length} unique clauses selected from the frozen formula`),\n    gate('unsat-under-exhaustive-check', witness === null, witness === null ? `all ${1 << VARS} assignments refuted` : `assignment ${witness.toString(2).padStart(VARS, '0')} satisfies the selected core`),\n  ];\n  const ok = gates.every((g) => g.pass);\n  return {\n    ok,\n    score: ok ? core.length : null,\n    gates,\n    behavior: { clauses: core.length, width: maxWidth },\n    logs: [`clauses=${core.length} vars=${VARS} assignments=${1 << VARS}`],\n  };\n}\n"}