TheoremDB

Problem packetWorkR18

R18artifactStatus: availableEvidence: ReproducedReplay: completeexhaustive over its scope

[#R18] Independent C++ exact search for {0,1,2,4}

View replay

1Summary

This independent C++20 implementation closes the full {0,1,2,4} search tree and returns the same node count, leaf count, maximum length, and two reversal-related maximizers.

The implementation uses a separate word representation and suffix-checking loop. It has a one-billion-node guard and a 300-second guard, and the tree closes far below both. The stable output digest removes runtime_seconds and preserves all other fields. A second operator reran the same tree in 0.71 seconds and matched every mathematical field.

Reproduced evidence. Recorded scope: all finite additive-square-free words over the exact integer alphabet {0,1,2,4}, including the empty word.

2Reproduce

Replay package: complete

The command, source, environment, and expected result are recorded.

clang++ -O3 -std=c++20 -Wall -Wextra -pedantic additive_square_search.cpp -o additive_square_search && ./additive_square_search
Entry point
Join source_lines with LF, append a terminal LF, and save as additive_square_search.cpp
Runtime
Apple clang 21.0.0, C++20 standard library, macOS 26.2 arm64
Dependencies
[ { "name": "Apple clang", "version": "21.0.0", "license": "Apache-2.0 WITH LLVM-exception" }, { "name": "Apple libc++", "version": "system C++20 library on macOS 26.2 arm64", "license": "Apache-2.0 WITH LLVM-exception" } ]
Recorded runtime
1.73

Verification source: Self-contained C++20 source authored and executed on macOS arm64 on 2026-07-28

Expected output

{
  "complete": true,
  "nodes": 19097778,
  "leaves": 5350440,
  "deepest_length": 62,
  "deepest_discovery_count": 2,
  "stable_output_sha256": "1fbb4953f87e9bbb8cc3332bd2b8b12157bc391d540eccc4eaa9476bd2ad5424",
  "deepest_words_integer_array_json_sha256": "f68304e459bafb73676c8d9e924434c7f2f1944d925403bca01b1bd2032a0179",
  "peak_resident_bytes_observed": 1441792
}

3Source code

View source code
Source code
#include <array>
#include <chrono>
#include <cstdint>
#include <cstdlib>
#include <iostream>
#include <vector>

using Clock = std::chrono::steady_clock;

static constexpr std::array<int, 4> alphabet{0, 1, 2, 4};
static constexpr std::uint64_t node_limit = 1000000000ULL;
static constexpr double second_limit = 300.0;

std::vector<int> word;
std::vector<long long> sums{0};
std::vector<int> best_word;
std::vector<std::vector<int>> best_words;
std::uint64_t nodes = 1;
std::uint64_t leaves = 0;
std::uint64_t best_count = 0;
bool stopped = false;
const auto started = Clock::now();

bool bad_suffix() {
    const int n = static_cast<int>(word.size());
    for (int half = 1; half <= n / 2; ++half) {
        const auto left = sums[n - half] - sums[n - 2 * half];
        const auto right = sums[n] - sums[n - half];
        if (left == right) return true;
    }
    return false;
}

void visit() {
    if (stopped) return;
    bool extended = false;
    for (const int value : alphabet) {
        word.push_back(value);
        sums.push_back(sums.back() + value);
        if (!bad_suffix()) {
            extended = true;
            ++nodes;
            if (word.size() > best_word.size()) {
                best_word = word;
                best_words = {word};
                best_count = 1;
            } else if (word.size() == best_word.size()) {
                best_words.push_back(word);
                ++best_count;
            }
            if (nodes >= node_limit) {
                stopped = true;
            } else if ((nodes & ((1ULL << 20) - 1)) == 0) {
                const double elapsed =
                    std::chrono::duration<double>(Clock::now() - started).count();
                if (nodes >= node_limit || elapsed >= second_limit) stopped = true;
            }
            if (!stopped) visit();
        }
        sums.pop_back();
        word.pop_back();
        if (stopped) return;
    }
    if (!extended) ++leaves;
}

int main() {
    visit();
    const double elapsed =
        std::chrono::duration<double>(Clock::now() - started).count();
    std::cout << "{\"alphabet\":[0,1,2,4],\"complete\":"
              << (stopped ? "false" : "true")
              << ",\"node_limit\":" << node_limit
              << ",\"second_limit\":" << second_limit
              << ",\"nodes\":" << nodes
              << ",\"leaves\":" << leaves
              << ",\"deepest_length\":" << best_word.size()
              << ",\"deepest_discovery_count\":" << best_count
              << ",\"runtime_seconds\":" << elapsed
              << ",\"deepest_words\":[";
    for (std::size_t item = 0; item < best_words.size(); ++item) {
        if (item) std::cout << ',';
        std::cout << '[';
        for (std::size_t index = 0; index < best_words[item].size(); ++index) {
            if (index) std::cout << ',';
            std::cout << best_words[item][index];
        }
        std::cout << ']';
    }
    std::cout << "]}\n";
}

4What it produced

Processor
Apple M4 arm64
Time bound
300 seconds wall clock, matching the program guard
Memory bound
128 MiB resident memory
Processor bound
one single-threaded native process
Source license
CC0-1.0
Network requirements
none
Memory bound bytes observed
1,441,792
Stopping rule
close the search tree, reach 1000000000 nodes, or reach the 300-second guard
Storage bound
2953-byte source, 55640-byte binary, and 460-byte stdout for the recorded command; no auxiliary data files
Execution date
2026-07-28
Source sha256
f0a098babc71aec690b78bc5450e9de9002caf4d1f553412a8f456030757b1bc
Recorded binary sha256
e49ff17b00e5ecf2676399cb7ba8f5f16662ff3811b99c011ce044640555678b
Binary digest scope
identity of the recorded executable; rebuilds may carry a different Mach-O linker UUID
Replay of
asq-artifact-python-exact-dfs
Independent operator runtime
0.71 seconds

Reproducibility anchors

source sha256f0a098babc71aec690b78bc5450e9de9002caf4d1f553412a8f456030757b1bcstable output sha2561fbb4953f87e9bbb8cc3332bd2b8b12157bc391d540eccc4eaa9476bd2ad5424

5How it connects

Recorded for

6Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R18",
  "content_hash": null,
  "slug": "asq-artifact-cpp-exact-dfs",
  "type": "artifact",
  "title": "Independent C++ exact search for {0,1,2,4}",
  "summary": "This independent C++20 implementation closes the full {0,1,2,4} search tree and returns the same node count, leaf count, maximum length, and two reversal-related maximizers.",
  "relevance": "For Infinite additive-square avoidance over a finite integer alphabet, record asq-artifact-cpp-exact-dfs (“Independent C++ exact search for {0,1,2,4}”) supplies evidence or a replay used to check the packet. The record states: This independent C++20 implementation closes the full {0,1,2,4} search tree and returns the same node count, leaf count, maximum length, and two reversal-related maximizers.",
  "relevance_source": "recorded",
  "body": "The implementation uses a separate word representation and suffix-checking loop. It has a one-billion-node guard and a 300-second guard, and the tree closes far below both. The stable output digest removes runtime_seconds and preserves all other fields. A second operator reran the same tree in 0.71 seconds and matched every mathematical field.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all finite additive-square-free words over the exact integer alphabet {0,1,2,4}, including the empty word",
    "bounds": {
      "alphabet_size": {
        "min": 4,
        "max": 4
      },
      "alphabet_maximum": {
        "min": 4,
        "max": 4
      },
      "word_length": {
        "min": 0,
        "max": 62
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_cpp_independent_exact_depth_first_enumerator",
    "command": "clang++ -O3 -std=c++20 -Wall -Wextra -pedantic additive_square_search.cpp -o additive_square_search && ./additive_square_search",
    "entrypoint": "Join source_lines with LF, append a terminal LF, and save as additive_square_search.cpp",
    "runtime": "Apple clang 21.0.0, C++20 standard library, macOS 26.2 arm64",
    "citation": {
      "locator": "Self-contained C++20 source authored and executed on macOS arm64 on 2026-07-28"
    },
    "dependencies": [
      {
        "name": "Apple clang",
        "version": "21.0.0",
        "license": "Apache-2.0 WITH LLVM-exception"
      },
      {
        "name": "Apple libc++",
        "version": "system C++20 library on macOS 26.2 arm64",
        "license": "Apache-2.0 WITH LLVM-exception"
      }
    ],
    "outputs": {
      "complete": true,
      "nodes": 19097778,
      "leaves": 5350440,
      "deepest_length": 62,
      "deepest_discovery_count": 2,
      "stable_output_sha256": "1fbb4953f87e9bbb8cc3332bd2b8b12157bc391d540eccc4eaa9476bd2ad5424",
      "deepest_words_integer_array_json_sha256": "f68304e459bafb73676c8d9e924434c7f2f1944d925403bca01b1bd2032a0179",
      "peak_resident_bytes_observed": 1441792
    },
    "runtime_seconds": 1.73,
    "inline_source": [
      "#include <array>",
      "#include <chrono>",
      "#include <cstdint>",
      "#include <cstdlib>",
      "#include <iostream>",
      "#include <vector>",
      "",
      "using Clock = std::chrono::steady_clock;",
      "",
      "static constexpr std::array<int, 4> alphabet{0, 1, 2, 4};",
      "static constexpr std::uint64_t node_limit = 1000000000ULL;",
      "static constexpr double second_limit = 300.0;",
      "",
      "std::vector<int> word;",
      "std::vector<long long> sums{0};",
      "std::vector<int> best_word;",
      "std::vector<std::vector<int>> best_words;",
      "std::uint64_t nodes = 1;",
      "std::uint64_t leaves = 0;",
      "std::uint64_t best_count = 0;",
      "bool stopped = false;",
      "const auto started = Clock::now();",
      "",
      "bool bad_suffix() {",
      "    const int n = static_cast<int>(word.size());",
      "    for (int half = 1; half <= n / 2; ++half) {",
      "        const auto left = sums[n - half] - sums[n - 2 * half];",
      "        const auto right = sums[n] - sums[n - half];",
      "        if (left == right) return true;",
      "    }",
      "    return false;",
      "}",
      "",
      "void visit() {",
      "    if (stopped) return;",
      "    bool extended = false;",
      "    for (const int value : alphabet) {",
      "        word.push_back(value);",
      "        sums.push_back(sums.back() + value);",
      "        if (!bad_suffix()) {",
      "            extended = true;",
      "            ++nodes;",
      "            if (word.size() > best_word.size()) {",
      "                best_word = word;",
      "                best_words = {word};",
      "                best_count = 1;",
      "            } else if (word.size() == best_word.size()) {",
      "                best_words.push_back(word);",
      "                ++best_count;",
      "            }",
      "            if (nodes >= node_limit) {",
      "                stopped = true;",
      "            } else if ((nodes & ((1ULL << 20) - 1)) == 0) {",
      "                const double elapsed =",
      "                    std::chrono::duration<double>(Clock::now() - started).count();",
      "                if (nodes >= node_limit || elapsed >= second_limit) stopped = true;",
      "            }",
      "            if (!stopped) visit();",
      "        }",
      "        sums.pop_back();",
      "        word.pop_back();",
      "        if (stopped) return;",
      "    }",
      "    if (!extended) ++leaves;",
      "}",
      "",
      "int main() {",
      "    visit();",
      "    const double elapsed =",
      "        std::chrono::duration<double>(Clock::now() - started).count();",
      "    std::cout << \"{\\\"alphabet\\\":[0,1,2,4],\\\"complete\\\":\"",
      "              << (stopped ? \"false\" : \"true\")",
      "              << \",\\\"node_limit\\\":\" << node_limit",
      "              << \",\\\"second_limit\\\":\" << second_limit",
      "              << \",\\\"nodes\\\":\" << nodes",
      "              << \",\\\"leaves\\\":\" << leaves",
      "              << \",\\\"deepest_length\\\":\" << best_word.size()",
      "              << \",\\\"deepest_discovery_count\\\":\" << best_count",
      "              << \",\\\"runtime_seconds\\\":\" << elapsed",
      "              << \",\\\"deepest_words\\\":[\";",
      "    for (std::size_t item = 0; item < best_words.size(); ++item) {",
      "        if (item) std::cout << ',';",
      "        std::cout << '[';",
      "        for (std::size_t index = 0; index < best_words[item].size(); ++index) {",
      "            if (index) std::cout << ',';",
      "            std::cout << best_words[item][index];",
      "        }",
      "        std::cout << ']';",
      "    }",
      "    std::cout << \"]}\\n\";",
      "}"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained C++20 source authored and executed on macOS arm64 on 2026-07-28"
  },
  "models": [],
  "relations": [
    {
      "slug": "R28",
      "title": "The exact finite maximum for {0,1,2,4} is 62",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "additive-square-finite-alphabet",
      "title": "additive square finite alphabet",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

7Provenance

View source, identifiers, and projection details
Project
additive-square-finite-alphabet-research
Locator
Self-contained C++20 source authored and executed on macOS arm64 on 2026-07-28
License
CC0-1.0
Public record
R18
Stable alias
asq-artifact-cpp-exact-dfs
Projection
Reproduction fields are derived from the immutable record.

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

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.