{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R556",
  "content_hash": null,
  "slug": "pcp5-artifact-chain-verifier",
  "type": "artifact",
  "title": "Exhaustive verifier for the 16-clause XOR chain",
  "summary": "The program proves the projected parity relation, visible-variable propagation completeness, and full nine-variable propagation completeness.",
  "relevance": "For Minimum propagation-complete CNF for five-bit parity, record pcp5-artifact-chain-verifier (“Exhaustive verifier for the 16-clause XOR chain”) supplies evidence or a replay used to check the packet. The record states: The program proves the projected parity relation, visible-variable propagation completeness, and full nine-variable propagation completeness.",
  "relevance_source": "recorded",
  "body": "Variables 1 through 6 are \\(x_1,x_2,x_3,x_4,x_5,y\\), and variables 7 through 9 are \\(z_1,z_2,z_3\\). For an equation \\(c=a\\oplus b\\), the verifier emits\n\\[\n(a\\vee b\\vee\\neg c),\\ (a\\vee\\neg b\\vee c),\\ (\\neg a\\vee b\\vee c),\\ (\\neg a\\vee\\neg b\\vee\\neg c).\n\\]\nIt applies this template to \\((x_1,x_2,z_1)\\), \\((z_1,x_3,z_2)\\), \\((z_2,x_4,z_3)\\), and \\((z_3,x_5,y)\\).\n\nThe semantic check enumerates all \\(2^9\\) total assignments. Exactly 32 satisfy the formula, their visible projections are exactly the 32 parity tuples, and every valid visible tuple has one auxiliary extension. For each ternary partial assignment, the program enumerates compatible total models. Unit propagation must find a conflict when that model set is empty and must derive every unassigned variable fixed across the compatible models.\n\nAmong the 729 visible partial assignments, 697 are consistent and 32 are inconsistent. There are 192 newly forced visible literals. Among all 19,683 partial assignments to the nine formula variables, 9,315 are consistent, 10,368 are inconsistent, and 21,960 unassigned literals are forced. Every obligation passes. The candidate record's number 2,916 is the total number of assigned visible positions across the 729 ternary rows, so it includes assumptions and inconsistent rows.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the specified 16-clause, nine-variable XOR-chain formula, checked under every partial assignment to the six visible variables and every partial assignment to all nine formula variables",
    "bounds": {
      "clauses": {
        "min": 16,
        "max": 16
      },
      "visible_partial_assignments": {
        "min": 729,
        "max": 729
      },
      "all_variable_partial_assignments": {
        "min": 19683,
        "max": 19683
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://doi.org/10.4230/LIPIcs.MFCS.2022.47",
      "locator": "Python 3 standard-library verifier executed by TheoremDB entry research on 2026-07-24"
    },
    "outputs": "models=32 clauses=16 sha256=5d623c4b742497aa7d599fa427e288e242e96c444763ea5c513fda7651c506ce visible=697/32/192 full=9315/10368/21960\n",
    "inline_source": [
      "import hashlib",
      "import itertools",
      "import json",
      "",
      "NAMES = ('x1', 'x2', 'x3', 'x4', 'x5', 'y', 'z1', 'z2', 'z3')",
      "",
      "def xor_gate(a, b, c):",
      "    return [(a, b, -c), (a, -b, c), (-a, b, c), (-a, -b, -c)]",
      "",
      "clauses = []",
      "for gate in ((1, 2, 7), (7, 3, 8), (8, 4, 9), (9, 5, 6)):",
      "    clauses.extend(xor_gate(*gate))",
      "assert len(clauses) == 16",
      "",
      "def satisfies(model):",
      "    return all(any(model[abs(lit) - 1] == (lit > 0) for lit in clause)",
      "               for clause in clauses)",
      "",
      "models = [bits for bits in itertools.product((False, True), repeat=9)",
      "          if satisfies(bits)]",
      "valid_visible = {bits for bits in itertools.product((False, True), repeat=6)",
      "                 if bits[5] == (sum(bits[:5]) % 2 == 1)}",
      "assert len(models) == 32",
      "assert {model[:6] for model in models} == valid_visible",
      "assert all(sum(model[:6] == visible for model in models) == 1",
      "           for visible in valid_visible)",
      "",
      "def propagate(partial):",
      "    assignment = {i: value for i, value in enumerate(partial)",
      "                  if value is not None}",
      "    while True:",
      "        changed = False",
      "        for clause in clauses:",
      "            if any(abs(lit) - 1 in assignment",
      "                   and assignment[abs(lit) - 1] == (lit > 0)",
      "                   for lit in clause):",
      "                continue",
      "            open_literals = [lit for lit in clause",
      "                             if abs(lit) - 1 not in assignment]",
      "            if not open_literals:",
      "                return None",
      "            if len(open_literals) == 1:",
      "                lit = open_literals[0]",
      "                assignment[abs(lit) - 1] = lit > 0",
      "                changed = True",
      "                break",
      "        if not changed:",
      "            return assignment",
      "",
      "def check(width):",
      "    consistent = 0",
      "    inconsistent = 0",
      "    forced_count = 0",
      "    for partial in itertools.product((None, False, True), repeat=width):",
      "        compatible = [model for model in models",
      "                      if all(value is None or model[i] == value",
      "                             for i, value in enumerate(partial))]",
      "        closure = propagate(partial + (None,) * (9 - width))",
      "        if not compatible:",
      "            inconsistent += 1",
      "            assert closure is None, (width, partial)",
      "            continue",
      "        consistent += 1",
      "        assert closure is not None",
      "        for i, value in enumerate(partial):",
      "            if value is not None:",
      "                continue",
      "            possible = {model[i] for model in compatible}",
      "            if len(possible) == 1:",
      "                forced = next(iter(possible))",
      "                forced_count += 1",
      "                assert closure.get(i) == forced, (width, partial, NAMES[i])",
      "    return consistent, inconsistent, forced_count",
      "",
      "visible = check(6)",
      "full = check(9)",
      "assert visible == (697, 32, 192)",
      "assert full == (9315, 10368, 21960)",
      "serialized = json.dumps(clauses, separators=(',', ':')).encode()",
      "digest = hashlib.sha256(serialized).hexdigest()",
      "assert digest == '5d623c4b742497aa7d599fa427e288e242e96c444763ea5c513fda7651c506ce'",
      "print(f'models={len(models)} clauses={len(clauses)} sha256={digest} '",
      "      f'visible={visible[0]}/{visible[1]}/{visible[2]} '",
      "      f'full={full[0]}/{full[1]}/{full[2]}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4230/LIPIcs.MFCS.2022.47",
    "locator": "Python 3 standard-library verifier executed by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R558",
      "title": "The certified interval is 9 to 16 clauses",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "propagation-complete-five-bit-parity",
      "title": "propagation complete five bit parity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}