{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R219",
  "content_hash": null,
  "slug": "dpb101-attempt-literature-and-exact-search-audit",
  "type": "attempt",
  "title": "The exact value at order 100 remains open in this audit",
  "summary": "Published exhaustive tables stop short of order 100, and the timeboxed size-17 SAT run produced no checkable conclusion.",
  "relevance": "For Minimum distinct-product basis of F_101, record dpb101-attempt-literature-and-exact-search-audit (“The exact value at order 100 remains open in this audit”) documents a concrete method, search boundary, or failed route. The record states: Published exhaustive tables stop short of order 100, and the timeboxed size-17 SAT run produced no checkable conclusion.",
  "relevance_source": "recorded",
  "body": "Haanpää calls a subset \\(S\\) of a finite abelian group a strict sum cover when every group element is \\(a+b\\) for distinct \\(a,b\\in S\\). This is exactly the exponent form of the present problem. His exhaustive backtracking computation covers abelian groups through order 90. Fitch and Jamison's earlier census covers cyclic groups through order 54. Neither published range reaches \\(\\mathbf Z/100\\mathbf Z\\).\n\nA 2021 discussion on Mathematics Stack Exchange posed \\(f_{\\rm cyc}(100)\\) as a concrete challenge with the same counting lower bound. A comment there establishes \\(f_+(100)=18\\) under a convention that only requires the nonzero classes. The present artifact independently checks all 100 classes required here.\n\nFor an exact test below 18, introduce Boolean variables \\(x_i\\) for selecting \\(i\\in\\mathbf Z/100\\mathbf Z\\). For every target \\(t\\), auxiliary variables encode the unordered pairs \\(\\{i,j\\}\\) with \\(i+j=t\\), and a coverage clause requires at least one such pair. Cardinality clauses impose at most 17 selected residues. Affine symmetry permits the normalization \\(x_0=x_1=1\\): every cover has a pair whose difference is coprime to 100, since otherwise the parity and modulo-5 projections force the set into one parity class or one residue class modulo 5. Translation and multiplication by the inverse difference send that pair to 0 and 1.\n\nThe normalized SAT runs exceeded the research timebox without returning a model or an unsatisfiability certificate. This is computational silence. It supplies no lower bound beyond 15. A complete size-17 model would improve the upper bound, while an independently replayable unsatisfiability certificate would reduce the remaining cases.",
  "status": "inconclusive",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "published strict-sum-cover tables and a timeboxed exact search for covers of Z/100Z with at most 17 elements, checked through 2026-07-24",
    "bounds": {
      "modulus": {
        "min": 100,
        "max": 100
      },
      "candidate_size": {
        "min": 15,
        "max": 17
      },
      "search_year": {
        "min": 2026,
        "max": 2026
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
      "locator": "Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, abstract and sections 1, 4, and 5; Mark A. Fitch and Robert E. Jamison, Minimum Sum Covers of Small Cyclic Groups, Congressus Numerantium 147 (2000), 65-81; focused exact-search run on 2026-07-24"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html",
    "locator": "Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, abstract and sections 1, 4, and 5; Mark A. Fitch and Robert E. Jamison, Minimum Sum Covers of Small Cyclic Groups, Congressus Numerantium 147 (2000), 65-81; focused exact-search run on 2026-07-24"
  },
  "models": [],
  "relations": [
    {
      "slug": "R220",
      "title": "The minimum lies between 15 and 18",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "distinct-product-basis-f101",
      "title": "distinct product basis f101",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}