{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R557",
  "content_hash": null,
  "slug": "pcp5-attempt-literature-and-exactness-audit",
  "type": "attempt",
  "title": "The checked literature leaves the exact clause count open",
  "summary": "Primary sources support the 16-clause construction and a 9-clause lower bound, with no located theorem closing the small-instance gap.",
  "relevance": "For Minimum propagation-complete CNF for five-bit parity, record pcp5-attempt-literature-and-exactness-audit (“The checked literature leaves the exact clause count open”) documents a concrete method, search boundary, or failed route. The record states: Primary sources support the 16-clause construction and a 9-clause lower bound, with no located theorem closing the small-instance gap.",
  "relevance_source": "recorded",
  "body": "Gwynne and Kullmann distinguish two propagation criteria. Their arc-consistency condition applies partial assignments to the variables of the represented XOR system and asks unit propagation to derive every forced original literal. Their propagation-completeness condition quantifies over all variables in the CNF, including auxiliaries. Under that terminology, the candidate's stated visible-variable condition is arc consistency. The 16-clause artifact passes both criteria, so the terminology does not affect its upper bound.\n\nThe same paper proves that the standard translation of one XOR equation is propagation complete. Its construction breaks a long XOR into binary equations with fresh variables, matching the four-gate chain checked here. Emdin et al. prove the unrestricted clause lower bound \\(3n-9\\), which yields 9 clauses at \\(n=6\\). Their limited-auxiliary estimates are asymptotic or width bounds and give no 16-clause lower bound for this fixed parameter choice.\n\nA focused search of these papers and their cited parity-encoding results found no exact clause minimum for six visible variables with at most three auxiliaries, under either propagation convention. This records the search result rather than a novelty theorem. A proof excluding 15 clauses, or an encoding with at most 15 clauses, would still meet the candidate's acceptance condition.",
  "status": "inconclusive",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "primary literature on existential CNF encodings of parity and unit-propagation quality, checked for an exact small-case result with six visible variables and at most three auxiliaries",
    "bounds": {
      "visible_variables": {
        "min": 6,
        "max": 6
      },
      "auxiliary_variables": {
        "min": 0,
        "max": 3
      },
      "audit_date": {
        "min": 20260724,
        "max": 20260724
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://arxiv.org/abs/1309.3060",
      "locator": "Matthew Gwynne and Oliver Kullmann, On SAT representations of XOR constraints, arXiv:1309.3060, definitions of AC and PC and Lemma 8.4; Emdin et al., CNF Encodings of Parity, MFCS 2022, Theorem 1.1"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1309.3060",
    "locator": "Matthew Gwynne and Oliver Kullmann, On SAT representations of XOR constraints, arXiv:1309.3060, definitions of AC and PC and Lemma 8.4; Emdin et al., CNF Encodings of Parity, MFCS 2022, Theorem 1.1"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R558",
      "title": "The certified interval is 9 to 16 clauses",
      "object_type": "claim",
      "relation": "informs",
      "direction": "outgoing"
    },
    {
      "slug": "propagation-complete-five-bit-parity",
      "title": "propagation complete five bit parity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}