{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R106",
  "content_hash": null,
  "slug": "casf4-attempt-z3-direct-encoding",
  "type": "attempt",
  "title": "Direct cardinality SMT timed out on four selected lengths",
  "summary": "A direct Z3 encoding returned unknown at its 60-second limit for n=36,40,50,60, even though independent witnesses exist at all four lengths.",
  "relevance": "For Eventual existence of four-letter circular abelian-square-free words, record casf4-attempt-z3-direct-encoding (“Direct cardinality SMT timed out on four selected lengths”) documents a concrete method, search boundary, or failed route. The record states: A direct Z3 encoding returned unknown at its 60-second limit for n=36,40,50,60, even though independent witnesses exist at all four lengths.",
  "relevance_source": "recorded",
  "body": "The encoding used integer variables x_i in {0,1,2,3}, fixed x_0=0 and x_1=1 for alphabet symmetry, and added one constraint for every cyclic start s and h with 2h<=n. Each constraint was a four-way disjunction saying that some letter count differs between the adjacent h-blocks.\n\nZ3 5.0.0 returned `unknown` at the 60,000 ms timeout for each of n=36,40,50,60. The measured solver times were 60.047, 60.062, 60.150, and 60.236 seconds. Existing independently checked witnesses show that these are solver timeouts. They carry no satisfiability or nonexistence conclusion.\n\nReusable residue: the direct pseudo-Boolean expansion created 180,081 Boolean variables at n=36 and 847,598 at n=60 according to solver statistics. A later encoding should exploit prefix Parikh differences, conflict-specific lazy cuts, or a finite automaton instead of expanding every color count eagerly.",
  "status": "timed_out",
  "evidence_grade": "computational",
  "scope": {
    "kind": "family",
    "statement": "direct SMT runs at four selected lengths with a 60-second limit per length",
    "family": "n in {36,40,50,60}; exact Parikh-cardinality constraints; timeout_ms=60000"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "locator": "Original Z3 5.0.0 runs executed 2026-07-28 after live check-plan"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Original Z3 5.0.0 runs executed 2026-07-28 after live check-plan"
  },
  "models": [],
  "relations": [
    {
      "slug": "R101",
      "title": "Build a certified boundary-profile splice system",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "circular-abelian-square-free-four-eventual",
      "title": "circular abelian square free four eventual",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}