{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R592",
  "content_hash": null,
  "slug": "pp12-artifact-model-audit",
  "type": "artifact",
  "title": "Exact OA and 11-MOLS computational formulation",
  "summary": "A 1,584-variable finite-domain model is equivalent to the required orthogonal array and has safe first-row and first-column symmetry breaking.",
  "relevance": "For A projective plane of order 12, record pp12-artifact-model-audit (“Exact OA and 11-MOLS computational formulation”) supplies evidence or a replay used to check the packet. The record states: A 1,584-variable finite-domain model is equivalent to the required orthogonal array and has safe first-row and first-column symmetry breaking.",
  "relevance_source": "recorded",
  "body": "Use integer variables\n\\[\nL_{k,r,c}\\in\\{0,\\ldots,11\\},\n\\quad 0\\le k<11,\\quad0\\le r,c<12.\n\\]\nFor each \\(k\\), impose `AllDifferent` on every row and every column of \\(L_k\\). This gives 264 Latin constraints. For each pair \\(k<\\ell\\), impose `AllDifferent` on the 144 values\n\\[\n12L_{k,r,c}+L_{\\ell,r,c}.\n\\]\nThere are 55 such constraints. Since every encoded value lies between 0 and 143, each constraint forces every ordered symbol pair to occur once. A satisfying assignment is exactly a complete family of 11 MOLS, or equivalently an \\(OA_1(144,13,12,2)\\).\n\nSafe normalization fixes \\(L_{k,0,c}=c\\) for every \\(k,c\\), then fixes \\(L_{0,r,0}=r\\) for \\(1\\le r<12\\). These are 143 fixed cells. They come from row and column permutations plus independent symbol relabeling. Any satisfying assignment constructs the plane. A complete unsatisfiability certificate for this normalized model proves nonexistence.\n\nThe inline program checks the design identities, the determinant value, the orthogonal-array dimensions, and the full constraint inventory. Its canonical report has SHA-256 digest `c980fe81ebe7fa46510d87f9c4c8f000f681b13eaff128ebb54bdfab7797feb1`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "parameter arithmetic and the complete constraint inventory for an 11-MOLS constraint-programming formulation at order 12",
    "bounds": {
      "order": {
        "min": 12,
        "max": 12
      },
      "integer_variables": {
        "min": 1584,
        "max": 1584
      },
      "all_different_constraints": {
        "min": 319,
        "max": 319
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.37236/11990",
      "locator": "The projective-plane, orthogonal-array, and complete-MOLS equivalences are standard and are used in Kharaghani and Suda, Electronic Journal of Combinatorics 30(2) (2023), P2.49; exact parameter audit executed 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from json import dumps",
      "from math import comb",
      "",
      "n = 12",
      "v = n*n + n + 1",
      "report = {",
      "    'order': n,",
      "    'points': v,",
      "    'lines': v,",
      "    'line_size': n + 1,",
      "    'incidences': v * (n + 1),",
      "    'point_pairs': comb(v, 2),",
      "    'pairs_covered_by_lines': v * comb(n + 1, 2),",
      "    'incidence_matrix_variables': v * v,",
      "    'incidence_matrix_equation': 'B B^T = 12 I_157 + J_157',",
      "    'determinant_absolute': 13 * 12**78,",
      "    'bruck_ryser_sum_two_squares_test_applies': n % 4 in (1, 2),",
      "    'oa': {",
      "        'rows': n*n,",
      "        'columns': n + 1,",
      "        'symbols': n,",
      "        'strength': 2,",
      "        'index': 1,",
      "        'column_pairs': comb(n + 1, 2),",
      "        'ordered_pair_checks': comb(n + 1, 2) * n*n,",
      "    },",
      "    'mols_cp_model': {",
      "        'squares': n - 1,",
      "        'integer_variables': (n - 1) * n*n,",
      "        'latin_all_different_constraints': 2 * (n - 1) * n,",
      "        'orthogonality_all_different_constraints': comb(n - 1, 2),",
      "        'total_all_different_constraints': 2 * (n - 1) * n + comb(n - 1, 2),",
      "        'normalized_fixed_cells': (n - 1) * n + (n - 1),",
      "    },",
      "}",
      "assert v == 157",
      "assert report['incidences'] == 2041",
      "assert report['point_pairs'] == report['pairs_covered_by_lines'] == 12246",
      "assert report['incidence_matrix_variables'] == 24649",
      "assert report['bruck_ryser_sum_two_squares_test_applies'] is False",
      "assert report['oa'] == {'rows': 144, 'columns': 13, 'symbols': 12, 'strength': 2, 'index': 1, 'column_pairs': 78, 'ordered_pair_checks': 11232}",
      "assert report['mols_cp_model'] == {'squares': 11, 'integer_variables': 1584, 'latin_all_different_constraints': 264, 'orthogonality_all_different_constraints': 55, 'total_all_different_constraints': 319, 'normalized_fixed_cells': 143}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "digest = sha256(payload.encode()).hexdigest()",
      "assert digest == 'c980fe81ebe7fa46510d87f9c4c8f000f681b13eaff128ebb54bdfab7797feb1'",
      "print(payload)",
      "print('report_sha256=' + digest)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.37236/11990",
    "locator": "The projective-plane, orthogonal-array, and complete-MOLS equivalences are standard and are used in Kharaghani and Suda, Electronic Journal of Combinatorics 30(2) (2023), P2.49; exact parameter audit executed 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R594",
      "title": "Bruck-Ryser gives no obstruction at order 12",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R597",
      "title": "Existence at order 12 remains open",
      "object_type": "claim",
      "relation": "reformulates",
      "direction": "outgoing"
    },
    {
      "slug": "projective-plane-order-12",
      "title": "projective plane order 12",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}