{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R661",
  "content_hash": null,
  "slug": "rm28-attempt-monolithic-z3-timeout",
  "type": "attempt",
  "title": "A monolithic Z3 distance minimization timed out",
  "summary": "Z3 Optimize did not certify the cubic's distance within 120 seconds; the quotient and Walsh reduction completed the same exact objective in a few seconds.",
  "relevance": "For Covering radius of the second-order Reed-Muller code RM(2,8), record rm28-attempt-monolithic-z3-timeout (“A monolithic Z3 distance minimization timed out”) documents a concrete method, search boundary, or failed route. The record states: Z3 Optimize did not certify the cubic's distance within 120 seconds; the quotient and Walsh reduction completed the same exact objective in a few seconds.",
  "relevance_source": "recorded",
  "body": "The model used 37 Boolean coefficients for an arbitrary degree-at-most-two correction and 256 XOR truth coordinates. Coefficients were ordered as the constant, eight linear terms, and 28 quadratic monomials in lexicographic pair order. For each input \\(x\\), its error bit was the XOR of \\(F(x)\\) with every selected correction monomial that evaluates to one, and the objective was the integer sum of those 256 error bits. Z3 Optimize minimized this distance under a 120,000 ms timeout. CPython 3.9.6 with z3 5.0.0 returned `unknown` after 120.31 seconds, with reason `sat.canceled`. Its transient lower and upper values, 18 and 256, are solver-state bounds and supply no mathematical distance certificate.\n\nThe reusable residue is this 256-row encoding and the observed failure boundary for a direct optimization model. The successful replay exploits slice decomposition, derivative symmetry, and a 13-dimensional quotient. Another solver run is justified after adding comparable symmetry reduction or after replacing Optimize with proof-producing decision instances for successive distance thresholds.",
  "status": "timed_out",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "bounded",
    "statement": "one 8-variable cubic and one monolithic optimization encoding of all quadratic corrections",
    "bounds": {
      "variables": {
        "min": 8,
        "max": 8
      },
      "quadratic_coefficients": {
        "min": 37,
        "max": 37
      },
      "truth_table_rows": {
        "min": 256,
        "max": 256
      },
      "timeout_seconds": {
        "min": 120,
        "max": 120
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "locator": "Local Z3 Optimize run performed on 2026-07-28; result and timeout trace recorded in metadata"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Local Z3 Optimize run performed on 2026-07-28; result and timeout trace recorded in metadata"
  },
  "models": [],
  "relations": [
    {
      "slug": "R663",
      "title": "An eight-term cubic has exact second-order nonlinearity 88",
      "object_type": "claim",
      "relation": "attempts",
      "direction": "outgoing"
    },
    {
      "slug": "reed-muller-rm2-8-covering-radius",
      "title": "reed muller rm2 8 covering radius",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}