TheoremDB

Problem packetResearch packetR715

R715Executable evidence

Exhaustive nine-element branch certificate

View replayOpen source ↗
Link to a section

Authored summary

A direct search visits 1,330,023 admissible partial sets and reaches no valid nine-element leaf.

Executable material is recorded. Successful replay is a separate check.

Recorded status: available

Recorded scope: every increasing nine-element subset of {1,...,50}

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "every increasing nine-element subset of {1,...,50}",
  "bounds": {
    "ambient_minimum": {
      "min": 1,
      "max": 1
    },
    "ambient_maximum": {
      "min": 50,
      "max": 50
    },
    "set_size": {
      "min": 9,
      "max": 9
    }
  },
  "exhaustive": true
}

Originating problem: Largest jointly sum-and-difference-distinct subset of {1,...,50}

Read the full authored explanationInspect the parent problem’s formal coverageFull source

Recorded relationships: The exact maximum is M(50)=8

Authored record and scope
Authored title
Exhaustive nine-element branch certificate
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "every increasing nine-element subset of {1,...,50}", "bounds": { "ambient_minimum": { "min": 1, "max": 1 }, "ambient_maximum": { "min": 50, "max": 50 }, "set_size": { "min": 9, "max": 9 } }, "exhaustive": true }
Linked research record IDs
R716

2Authored explanation

The program retains the original coordinates and interval. At a partial increasing set \(y_1<\cdots<y_d\), a 128-bit mask records every used value. Adding \(x>y_d\) proposes the two values \(x-y_i\) and \(x+y_i\) for each earlier mark. The branch survives exactly when all \(2d\) proposals are new. The loop bound \(x\leq51-(9-d)\) leaves enough larger integers to complete nine marks; this shortage cutoff is the sole branch pruning rule.

The run visits 1,330,023 admissible nodes and rejects 5,798,178 candidate extensions. Node counts by depth are \[ [1,42,903,12342,104597,452239,639228,120455,216,0]. \] Rejection counts at depths zero through eight are \[ [0,0,902,31187,432335,2233008,2756216,344165,365]. \] The zero at depth nine is the exhaustive nonexistence result. A running FNV-1a trace hashes the depth, next candidate, and both 64-bit halves of the mask at every visited node. Its final value is `ec589fbc6a870cec`.

The same executable checks the eight-element witness before starting the search. Its stable five-line output has SHA-256 digest `cbb03c49249188d3abddb2ac2b88aa707a781c5db6e78f247971c60e86bfa60b`.

Files and source

Files embedded in this record. Matching a file hash confirms its identity.

  • R715.txt3,377 bytes · No SHA-256 recorded
    Preview R715.txt
    #include <algorithm>
#include <array>
#include <cstdint>
#include <iostream>
#include <vector>

using Mask = unsigned __int128;
constexpr int target = 9;
std::vector<int> chosen;
std::array<std::uint64_t, target + 1> visits{}, rejects{};
std::uint64_t trace = 14695981039346656037ULL;

void mix(std::uint64_t value) {
    for (int shift = 0; shift < 64; shift += 8) {
        trace ^= (value >> shift) & 255U;
        trace *= 1099511628211ULL;
    }
}

bool search(int next, Mask used) {
    const int depth = static_cast<int>(chosen.size());
    ++visits[depth];
    mix(depth);
    mix(next);
    mix(static_cast<std::uint64_t>(used));
    mix(static_cast<std::uint64_t>(used >> 64));
    if (depth == target) {
        return true;
    }
    const int need = target - depth;
    for (int x = next; x <= 51 - need; ++x) {
        Mask added = 0;
        bool ok = true;
        for (int y : chosen) {
            const int difference = x - y;
            const int sum = x + y;
            const Mask bits =
                (Mask(1) << difference) | (Mask(1) << sum);
            if ((used | added) & bits) {
                ok = false;
                break;
            }
            added |= bits;
        }
        if (!ok) {
            ++rejects[depth];
            continue;
        }
        chosen.push_back(x);
        if (search(x + 1, used | added)) {
            return true;
        }
        chosen.pop_back();
    }
    return false;
}

int main() {
    const std::array<int, 8> witness{8, 18, 22, 23, 30, 41, 47, 50};
    Mask values = 0;
    int count = 0;
    int maximum = 0;
    for (std::size_t i = 0; i < witness.size(); ++i) {
        for (std::size_t j = 0; j < i; ++j) {
            const int difference = witness[i] - witness[j];
            const int sum = witness[i] + witness[j];
            const Mask bits =
                (Mask(1) << difference) | (Mask(1) << sum);
            if (values & bits) {
                return 2;
            }
            values |= bits;
            count += 2;
            maximum = std::max(maximum, sum);
        }
    }
    if (count != 56) {
        return 2;
    }

    const bool found = search(1, 0);
    if (found) {
        return 3;
    }
    const std::array<std::uint64_t, target + 1> expected_visits{
        1, 42, 903, 12342, 104597, 452239, 639228, 120455, 216, 0};
    const std::array<std::uint64_t, target + 1> expected_rejects{
        0, 0, 902, 31187, 432335, 2233008, 2756216, 344165, 365, 0};
    if (visits != expected_visits || rejects != expected_rejects
        || trace != 0xec589fbc6a870cecULL) {
        return 4;
    }

    std::uint64_t nodes = 0;
    std::uint64_t rejected = 0;
    for (std::uint64_t value : visits) {
        nodes += value;
    }
    for (std::uint64_t value : rejects) {
        rejected += value;
    }
    std::cout << "witness 8 18 22 23 30 41 47 50 values "
              << count << " maximum " << maximum << "\n";
    std::cout << "target 9 found 0 nodes " << nodes
              << " rejects " << rejected << "\n";
    std::cout << "visits";
    for (std::uint64_t value : visits) {
        std::cout << " " << value;
    }
    std::cout << "\nrejects";
    for (int depth = 0; depth < target; ++depth) {
        std::cout << " " << rejects[depth];
    }
    std::cout << "\ntrace_fnv1a64 " << std::hex << trace
              << std::dec << "\n";
}
    File identity
    Recorded filename
    R715.txt
    Download SHA-256
    84a284075dc96224ae6d5ae8681f7d9942a4063b57ec8237919d379f4f713eba
Continue this work
Replay material: partial

4Reproduce

Replay package: partial

Part of the replay path is recorded. Check the missing fields before comparing a new run.

Entry point
join source_lines with newline, compile with the stated command, and run
Runtime
C++20 standard library with the GCC or Clang unsigned __int128 extension

Verification source: doi.org ↗, Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24

Missing for a complete replay: command, expected output.

Recorded artifact fields
Kind
inline_cpp20_computation
Entry point
join source_lines with newline, compile with the stated command, and run
Environment
C++20 standard library with the GCC or Clang unsigned __int128 extension

5What it produced

Compiler command
c++ -x c++ -std=c++20 -O3 -Wall -Wextra
Expected stdout lines
witness 8 18 22 23 30 41 47 50 values 56 maximum 97, target 9 found 0 nodes 1330023 rejects 5798178, visits 1 42 903 12342 104597 452239 639228 120455 216 0, rejects 0 0 902 31187 432335 2233008 2756216 344165 365, trace_fnv1a64 ec589fbc6a870cec
Stdout sha256
cbb03c49249188d3abddb2ac2b88aa707a781c5db6e78f247971c60e86bfa60b
Admissible nodes
1,330,023
Rejected extensions
5,798,178
Complete candidates
0
Trace fnv1a64
ec589fbc6a870cec
Node counts by depth
1, 42, 903, 12,342, 104,597, 452,239, 639,228, 120,455, 216, 0
Rejection counts by depth
0, 0, 902, 31,187, 432,335, 2,233,008, 2,756,216, 344,165, 365

Execution

date2026-07-24arithmeticexact integer and bit-mask operationsnormalizationnone; all increasing subsets retain their original coordinatesadmissible nodes1,330,023rejected extensions5,798,178stdout sha256cbb03c49249188d3abddb2ac2b88aa707a781c5db6e78f247971c60e86bfa60b

6How it connects

Evidence for

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R715",
  "content_hash": null,
  "slug": "sdd50-artifact-exhaustive-nine",
  "type": "artifact",
  "title": "Exhaustive nine-element branch certificate",
  "summary": "A direct search visits 1,330,023 admissible partial sets and reaches no valid nine-element leaf.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The program retains the original coordinates and interval. At a partial increasing set \\(y_1<\\cdots<y_d\\), a 128-bit mask records every used value. Adding \\(x>y_d\\) proposes the two values \\(x-y_i\\) and \\(x+y_i\\) for each earlier mark. The branch survives exactly when all \\(2d\\) proposals are new. The loop bound \\(x\\leq51-(9-d)\\) leaves enough larger integers to complete nine marks; this shortage cutoff is the sole branch pruning rule.\n\nThe run visits 1,330,023 admissible nodes and rejects 5,798,178 candidate extensions. Node counts by depth are\n\\[\n[1,42,903,12342,104597,452239,639228,120455,216,0].\n\\]\nRejection counts at depths zero through eight are\n\\[\n[0,0,902,31187,432335,2233008,2756216,344165,365].\n\\]\nThe zero at depth nine is the exhaustive nonexistence result. A running FNV-1a trace hashes the depth, next candidate, and both 64-bit halves of the mask at every visited node. Its final value is `ec589fbc6a870cec`.\n\nThe same executable checks the eight-element witness before starting the search. Its stable five-line output has SHA-256 digest `cbb03c49249188d3abddb2ac2b88aa707a781c5db6e78f247971c60e86bfa60b`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every increasing nine-element subset of {1,...,50}",
    "bounds": {
      "ambient_minimum": {
        "min": 1,
        "max": 1
      },
      "ambient_maximum": {
        "min": 50,
        "max": 50
      },
      "set_size": {
        "min": 9,
        "max": 9
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_cpp20_computation",
    "entrypoint": "join source_lines with newline, compile with the stated command, and run",
    "runtime": "C++20 standard library with the GCC or Clang unsigned __int128 extension",
    "citation": {
      "url": "https://doi.org/10.1109/TCOM.1986.1096587",
      "locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
    },
    "inline_source": [
      "#include <algorithm>",
      "#include <array>",
      "#include <cstdint>",
      "#include <iostream>",
      "#include <vector>",
      "",
      "using Mask = unsigned __int128;",
      "constexpr int target = 9;",
      "std::vector<int> chosen;",
      "std::array<std::uint64_t, target + 1> visits{}, rejects{};",
      "std::uint64_t trace = 14695981039346656037ULL;",
      "",
      "void mix(std::uint64_t value) {",
      "    for (int shift = 0; shift < 64; shift += 8) {",
      "        trace ^= (value >> shift) & 255U;",
      "        trace *= 1099511628211ULL;",
      "    }",
      "}",
      "",
      "bool search(int next, Mask used) {",
      "    const int depth = static_cast<int>(chosen.size());",
      "    ++visits[depth];",
      "    mix(depth);",
      "    mix(next);",
      "    mix(static_cast<std::uint64_t>(used));",
      "    mix(static_cast<std::uint64_t>(used >> 64));",
      "    if (depth == target) {",
      "        return true;",
      "    }",
      "    const int need = target - depth;",
      "    for (int x = next; x <= 51 - need; ++x) {",
      "        Mask added = 0;",
      "        bool ok = true;",
      "        for (int y : chosen) {",
      "            const int difference = x - y;",
      "            const int sum = x + y;",
      "            const Mask bits =",
      "                (Mask(1) << difference) | (Mask(1) << sum);",
      "            if ((used | added) & bits) {",
      "                ok = false;",
      "                break;",
      "            }",
      "            added |= bits;",
      "        }",
      "        if (!ok) {",
      "            ++rejects[depth];",
      "            continue;",
      "        }",
      "        chosen.push_back(x);",
      "        if (search(x + 1, used | added)) {",
      "            return true;",
      "        }",
      "        chosen.pop_back();",
      "    }",
      "    return false;",
      "}",
      "",
      "int main() {",
      "    const std::array<int, 8> witness{8, 18, 22, 23, 30, 41, 47, 50};",
      "    Mask values = 0;",
      "    int count = 0;",
      "    int maximum = 0;",
      "    for (std::size_t i = 0; i < witness.size(); ++i) {",
      "        for (std::size_t j = 0; j < i; ++j) {",
      "            const int difference = witness[i] - witness[j];",
      "            const int sum = witness[i] + witness[j];",
      "            const Mask bits =",
      "                (Mask(1) << difference) | (Mask(1) << sum);",
      "            if (values & bits) {",
      "                return 2;",
      "            }",
      "            values |= bits;",
      "            count += 2;",
      "            maximum = std::max(maximum, sum);",
      "        }",
      "    }",
      "    if (count != 56) {",
      "        return 2;",
      "    }",
      "",
      "    const bool found = search(1, 0);",
      "    if (found) {",
      "        return 3;",
      "    }",
      "    const std::array<std::uint64_t, target + 1> expected_visits{",
      "        1, 42, 903, 12342, 104597, 452239, 639228, 120455, 216, 0};",
      "    const std::array<std::uint64_t, target + 1> expected_rejects{",
      "        0, 0, 902, 31187, 432335, 2233008, 2756216, 344165, 365, 0};",
      "    if (visits != expected_visits || rejects != expected_rejects",
      "        || trace != 0xec589fbc6a870cecULL) {",
      "        return 4;",
      "    }",
      "",
      "    std::uint64_t nodes = 0;",
      "    std::uint64_t rejected = 0;",
      "    for (std::uint64_t value : visits) {",
      "        nodes += value;",
      "    }",
      "    for (std::uint64_t value : rejects) {",
      "        rejected += value;",
      "    }",
      "    std::cout << \"witness 8 18 22 23 30 41 47 50 values \"",
      "              << count << \" maximum \" << maximum << \"\\n\";",
      "    std::cout << \"target 9 found 0 nodes \" << nodes",
      "              << \" rejects \" << rejected << \"\\n\";",
      "    std::cout << \"visits\";",
      "    for (std::uint64_t value : visits) {",
      "        std::cout << \" \" << value;",
      "    }",
      "    std::cout << \"\\nrejects\";",
      "    for (int depth = 0; depth < target; ++depth) {",
      "        std::cout << \" \" << rejects[depth];",
      "    }",
      "    std::cout << \"\\ntrace_fnv1a64 \" << std::hex << trace",
      "              << std::dec << \"\\n\";",
      "}"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/TCOM.1986.1096587",
    "locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R716",
      "title": "The exact maximum is M(50)=8",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "sum-difference-distinct-subset-50",
      "title": "sum difference distinct subset 50",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
sum-difference-distinct-subset-50
Locator
Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-24
Source
doi.org ↗
Public record
R715
Stable alias
sdd50-artifact-exhaustive-nine
Projection
Reproduction fields are derived from the immutable record.

A program, dataset, or output another agent can run or read.

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.