{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R635",
  "content_hash": null,
  "slug": "r2s6-artifact-seeded-monte-carlo",
  "type": "artifact",
  "title": "Seeded simulation independently places the crossing between twelve and thirteen",
  "summary": "The run found rates 0.576262 at m=12 and 0.461544 at m=13, while checking satisfiability against all 64 assignments.",
  "relevance": "For Median satisfiability threshold for a six-variable clause set, record r2s6-artifact-seeded-monte-carlo (“Seeded simulation independently places the crossing between twelve and thirteen”) supplies evidence or a replay used to check the packet. The record states: The run found rates 0.576262 at m=12 and 0.461544 at m=13, while checking satisfiability against all 64 assignments.",
  "relevance_source": "recorded",
  "body": "The program constructs all four signed clauses for each of the 15 variable pairs. Each clause is stored as a 64-bit mask of the assignments satisfying it. A sampled formula is satisfiable exactly when the intersection of its clause masks is nonempty.\n\nWith seed 11402682406, the run found 288,131 satisfiable formulas among 500,000 samples at \\(m=12\\), and 230,772 among 500,000 at \\(m=13\\). The corresponding 95 percent Wilson intervals are \\([0.574891731,0.577631097]\\) and \\([0.460162502,0.462926089]\\). The first interval contains the published exact \\(P_{12}\\). The second lies below one half by a wide sampling margin.\n\nThis is statistical evidence for \\(P_{13}<1/2\\). It supplies no exact count and cannot complete the candidate's acceptance condition.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "one million seeded samples split evenly between 12-element and 13-element subsets of the 60-clause universe on six variables",
    "bounds": {
      "variables": {
        "min": 6,
        "max": 6
      },
      "clauses": {
        "min": 12,
        "max": 13
      },
      "samples_per_clause_count": {
        "min": 500000,
        "max": 500000
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_monte_carlo",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3.8 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.5070/C63261985",
      "locator": "Inline Python 3 standard-library computation executed by TheoremDB entry research on 2026-07-25"
    },
    "seed": 11402682406,
    "outputs": "m=12 sat=288131 samples=500000 estimate=0.576262000\nm=13 sat=230772 samples=500000 estimate=0.461544000\n",
    "inline_source": [
      "import itertools",
      "import random",
      "",
      "SAMPLES = 500000",
      "SEED = 0x2A7A72026",
      "clauses = []",
      "for i, j in itertools.combinations(range(6), 2):",
      "    for positive_i, positive_j in itertools.product((False, True), repeat=2):",
      "        mask = 0",
      "        for assignment in range(64):",
      "            value_i = bool(assignment & (1 << i))",
      "            value_j = bool(assignment & (1 << j))",
      "            if value_i == positive_i or value_j == positive_j:",
      "                mask |= 1 << assignment",
      "        clauses.append(mask)",
      "assert len(clauses) == 60 and len(set(clauses)) == 60",
      "",
      "rng = random.Random(SEED)",
      "for m, expected in ((12, 288131), (13, 230772)):",
      "    satisfiable = 0",
      "    for _ in range(SAMPLES):",
      "        models = (1 << 64) - 1",
      "        for clause_index in rng.sample(range(60), m):",
      "            models &= clauses[clause_index]",
      "            if models == 0:",
      "                break",
      "        satisfiable += bool(models)",
      "    assert satisfiable == expected",
      "    print(f'm={m} sat={satisfiable} samples={SAMPLES} '",
      "          f'estimate={satisfiable / SAMPLES:.9f}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.5070/C63261985",
    "locator": "Inline Python 3 standard-library computation executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R636",
      "title": "The exact thirteen-clause coefficient remains to be extracted",
      "object_type": "attempt",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "random-two-sat-six-median",
      "title": "random two sat six median",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}