TheoremDB

Problem packetResearch packetR421

R421Executable evidence

Complete eleven-point independent-set certificate

View replayOpen source ↗
Link to a section

Authored summary

The search visits 991,485 admissible partial sets and finds no independent set of size eleven.

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

Recorded status: available

Recorded scope: every eleven-element subset of the 49 points in {0,...,6}^2 under the possibly-flat isosceles convention

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "every eleven-element subset of the 49 points in {0,...,6}^2 under the possibly-flat isosceles convention",
  "bounds": {
    "coordinate_minimum": {
      "min": 0,
      "max": 0
    },
    "coordinate_maximum": {
      "min": 6,
      "max": 6
    },
    "candidate_points": {
      "min": 49,
      "max": 49
    },
    "set_size": {
      "min": 11,
      "max": 11
    }
  },
  "exhaustive": true
}

Originating problem: Largest isosceles-triangle-free subset of the 7 by 7 grid

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

Recorded relationships: The exact maximum is I_7=10

Authored record and scope
Authored title
Complete eleven-point independent-set certificate
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "every eleven-element subset of the 49 points in {0,...,6}^2 under the possibly-flat isosceles convention", "bounds": { "coordinate_minimum": { "min": 0, "max": 0 }, "coordinate_maximum": { "min": 6, "max": 6 }, "candidate_points": { "min": 49, "max": 49 }, "set_size": { "min": 11, "max": 11 } }, "exhaustive": true }
Linked research record IDs
R423

2Authored explanation

The program orders points first by \(x\), then by \(y\). It enumerates all \(\binom{49}{3}=18{,}424\) triples and marks the 2,488 whose squared-distance multiset has fewer than three values. Serializing each marked triple as its three one-byte vertex indices gives FNV-1a digest `b36e0b83c873e23f`.

The depth-first search adds vertices in increasing order, so each eleven-set has one branch. Every extension is tested against all selected vertex pairs. The only cutoff is the shortage of later vertices needed to reach eleven. The run visits 991,485 admissible nodes and rejects 4,354,134 extensions that complete a forbidden triple. Node counts by selected-set size are \[ [1,39,780,9035,59093,205914,353328,267906,84906,10035,448,0]. \] The final zero is the exhaustive nonexistence result. A running FNV-1a trace of each visited node's depth, next index, and 49-bit selected mask ends at `1ece71b42de90c50`.

The same executable checks all 120 triples in the ten-point witness before searching. Its stable six-line output has SHA-256 digest `ae59f5df2c114c75acb584c00390969aae589e9606cbde7d1d3cd50e0a854519`.

Files and source

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

  • R421.txt4,929 bytes · No SHA-256 recorded
    Preview R421.txt
    #include <array>
#include <cstdint>
#include <iostream>
#include <vector>

struct Point { int x; int y; };
constexpr int side = 7;
constexpr int point_count = 49;
constexpr int target = 11;
std::array<Point, point_count> points{};
std::array<std::array<std::array<unsigned char, point_count>,
                      point_count>, point_count> forbidden{};
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;
    }
}

int distance2(Point a, Point b) {
    const int x = a.x - b.x;
    const int y = a.y - b.y;
    return x*x + y*y;
}

bool is_forbidden(int a, int b, int c) {
    const int x = distance2(points[a],points[b]);
    const int y = distance2(points[a],points[c]);
    const int z = distance2(points[b],points[c]);
    return x == y || x == z || y == z;
}

bool search(int next, std::uint64_t selected) {
    const int depth = static_cast<int>(chosen.size());
    ++visits[depth];
    mix(depth);
    mix(next);
    mix(selected);
    if (depth == target) {
        return true;
    }
    const int need = target - depth;
    for (int candidate = next;
         candidate <= point_count - need;
         ++candidate) {
        bool ok = true;
        for (int i = 0; i < depth && ok; ++i) {
            for (int j = i + 1; j < depth; ++j) {
                if (forbidden[chosen[i]][chosen[j]][candidate]) {
                    ok = false;
                    break;
                }
            }
        }
        if (!ok) {
            ++rejects[depth];
            continue;
        }
        chosen.push_back(candidate);
        if (search(
            candidate + 1,
            selected | (UINT64_C(1) << candidate)
        )) {
            return true;
        }
        chosen.pop_back();
    }
    return false;
}

int main() {
    int index = 0;
    for (int x = 0; x < side; ++x) {
        for (int y = 0; y < side; ++y) {
            points[index++] = {x,y};
        }
    }

    std::uint64_t edge_hash = 14695981039346656037ULL;
    int edge_count = 0;
    for (int a = 0; a < point_count; ++a) {
        for (int b = a + 1; b < point_count; ++b) {
            for (int c = b + 1; c < point_count; ++c) {
                if (!is_forbidden(a,b,c)) continue;
                ++edge_count;
                for (int value : {a,b,c}) {
                    edge_hash ^= value;
                    edge_hash *= 1099511628211ULL;
                }
                for (int i : {a,b,c}) {
                    for (int j : {a,b,c}) {
                        for (int k : {a,b,c}) {
                            if (i != j && i != k && j != k) {
                                forbidden[i][j][k] = 1;
                            }
                        }
                    }
                }
            }
        }
    }

    const std::array<Point, 10> witness{{
        {0,0},{0,1},{0,3},{0,4},{1,6},
        {2,6},{5,5},{5,6},{6,3},{6,4}
    }};
    int checked = 0;
    for (int a = 0; a < 10; ++a) {
        for (int b = a + 1; b < 10; ++b) {
            for (int c = b + 1; c < 10; ++c) {
                const int x = distance2(witness[a],witness[b]);
                const int y = distance2(witness[a],witness[c]);
                const int z = distance2(witness[b],witness[c]);
                if (x == y || x == z || y == z) return 2;
                ++checked;
            }
        }
    }
    if (checked != 120 || edge_count != 2488
        || edge_hash != 0xb36e0b83c873e23fULL) {
        return 2;
    }

    const bool found = search(0,0);
    const std::array<std::uint64_t, target + 1> expected_visits{
        1,39,780,9035,59093,205914,353328,267906,84906,10035,448,0
    };
    const std::array<std::uint64_t, target + 1> expected_rejects{
        0,0,1625,34375,280362,996123,1589251,1100072,318265,32717,1344,0
    };
    if (found || visits != expected_visits
        || rejects != expected_rejects
        || trace != 0x1ece71b42de90c50ULL) {
        return 3;
    }

    std::uint64_t nodes = 0;
    std::uint64_t rejected = 0;
    for (auto value : visits) nodes += value;
    for (auto value : rejects) rejected += value;
    std::cout << "witness 10 triples " << checked << " conflicts 0\n";
    std::cout << "hypergraph vertices 49 edges " << edge_count
              << " fnv1a64 " << std::hex << edge_hash << std::dec << "\n";
    std::cout << "target 11 found 0 nodes " << nodes
              << " rejects " << rejected << "\n";
    std::cout << "visits";
    for (auto 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
    R421.txt
    Download SHA-256
    791d1a5f2b952e5d27e1169b1bfecf074ee818e7f049218b5952a79f5cf3c83c
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
ISO C++20 standard library

Verification source: arxiv.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
ISO C++20 standard library

5What it produced

Compiler command
c++ -x c++ -std=c++20 -O3 -Wall -Wextra
Expected stdout lines
witness 10 triples 120 conflicts 0, hypergraph vertices 49 edges 2488 fnv1a64 b36e0b83c873e23f, target 11 found 0 nodes 991485 rejects 4354134, visits 1 39 780 9035 59093 205914 353328 267906 84906 10035 448 0, rejects 0 0 1625 34375 280362 996123 1589251 1100072 318265 32717 1344, trace_fnv1a64 1ece71b42de90c50
Stdout sha256
ae59f5df2c114c75acb584c00390969aae589e9606cbde7d1d3cd50e0a854519
Candidate extensions
5,345,618
Admissible nodes
991,485
Rejected extensions
4,354,134
Complete candidates
0
Hypergraph edges
2,488
Hypergraph fnv1a64
b36e0b83c873e23f
Trace fnv1a64
1ece71b42de90c50
Node counts by depth
1, 39, 780, 9,035, 59,093, 205,914, 353,328, 267,906, 84,906, 10,035, 448, 0
Rejection counts by depth
0, 0, 1,625, 34,375, 280,362, 996,123, 1,589,251, 1,100,072, 318,265, 32,717, 1,344

Execution

date2026-07-24arithmeticexact integer squared distances and a 49-bit selected masksymmetry reductionnoneadmissible nodes991,485stdout sha256ae59f5df2c114c75acb584c00390969aae589e9606cbde7d1d3cd50e0a854519

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": "R421",
  "content_hash": null,
  "slug": "iso7-artifact-complete-eleven-search",
  "type": "artifact",
  "title": "Complete eleven-point independent-set certificate",
  "summary": "The search visits 991,485 admissible partial sets and finds no independent set of size eleven.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The program orders points first by \\(x\\), then by \\(y\\). It enumerates all \\(\\binom{49}{3}=18{,}424\\) triples and marks the 2,488 whose squared-distance multiset has fewer than three values. Serializing each marked triple as its three one-byte vertex indices gives FNV-1a digest `b36e0b83c873e23f`.\n\nThe depth-first search adds vertices in increasing order, so each eleven-set has one branch. Every extension is tested against all selected vertex pairs. The only cutoff is the shortage of later vertices needed to reach eleven. The run visits 991,485 admissible nodes and rejects 4,354,134 extensions that complete a forbidden triple. Node counts by selected-set size are\n\\[\n[1,39,780,9035,59093,205914,353328,267906,84906,10035,448,0].\n\\]\nThe final zero is the exhaustive nonexistence result. A running FNV-1a trace of each visited node's depth, next index, and 49-bit selected mask ends at `1ece71b42de90c50`.\n\nThe same executable checks all 120 triples in the ten-point witness before searching. Its stable six-line output has SHA-256 digest `ae59f5df2c114c75acb584c00390969aae589e9606cbde7d1d3cd50e0a854519`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every eleven-element subset of the 49 points in {0,...,6}^2 under the possibly-flat isosceles convention",
    "bounds": {
      "coordinate_minimum": {
        "min": 0,
        "max": 0
      },
      "coordinate_maximum": {
        "min": 6,
        "max": 6
      },
      "candidate_points": {
        "min": 49,
        "max": 49
      },
      "set_size": {
        "min": 11,
        "max": 11
      }
    },
    "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": "ISO C++20 standard library",
    "citation": {
      "url": "https://arxiv.org/abs/2411.00566",
      "locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
    },
    "inline_source": [
      "#include <array>",
      "#include <cstdint>",
      "#include <iostream>",
      "#include <vector>",
      "",
      "struct Point { int x; int y; };",
      "constexpr int side = 7;",
      "constexpr int point_count = 49;",
      "constexpr int target = 11;",
      "std::array<Point, point_count> points{};",
      "std::array<std::array<std::array<unsigned char, point_count>,",
      "                      point_count>, point_count> forbidden{};",
      "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;",
      "    }",
      "}",
      "",
      "int distance2(Point a, Point b) {",
      "    const int x = a.x - b.x;",
      "    const int y = a.y - b.y;",
      "    return x*x + y*y;",
      "}",
      "",
      "bool is_forbidden(int a, int b, int c) {",
      "    const int x = distance2(points[a],points[b]);",
      "    const int y = distance2(points[a],points[c]);",
      "    const int z = distance2(points[b],points[c]);",
      "    return x == y || x == z || y == z;",
      "}",
      "",
      "bool search(int next, std::uint64_t selected) {",
      "    const int depth = static_cast<int>(chosen.size());",
      "    ++visits[depth];",
      "    mix(depth);",
      "    mix(next);",
      "    mix(selected);",
      "    if (depth == target) {",
      "        return true;",
      "    }",
      "    const int need = target - depth;",
      "    for (int candidate = next;",
      "         candidate <= point_count - need;",
      "         ++candidate) {",
      "        bool ok = true;",
      "        for (int i = 0; i < depth && ok; ++i) {",
      "            for (int j = i + 1; j < depth; ++j) {",
      "                if (forbidden[chosen[i]][chosen[j]][candidate]) {",
      "                    ok = false;",
      "                    break;",
      "                }",
      "            }",
      "        }",
      "        if (!ok) {",
      "            ++rejects[depth];",
      "            continue;",
      "        }",
      "        chosen.push_back(candidate);",
      "        if (search(",
      "            candidate + 1,",
      "            selected | (UINT64_C(1) << candidate)",
      "        )) {",
      "            return true;",
      "        }",
      "        chosen.pop_back();",
      "    }",
      "    return false;",
      "}",
      "",
      "int main() {",
      "    int index = 0;",
      "    for (int x = 0; x < side; ++x) {",
      "        for (int y = 0; y < side; ++y) {",
      "            points[index++] = {x,y};",
      "        }",
      "    }",
      "",
      "    std::uint64_t edge_hash = 14695981039346656037ULL;",
      "    int edge_count = 0;",
      "    for (int a = 0; a < point_count; ++a) {",
      "        for (int b = a + 1; b < point_count; ++b) {",
      "            for (int c = b + 1; c < point_count; ++c) {",
      "                if (!is_forbidden(a,b,c)) continue;",
      "                ++edge_count;",
      "                for (int value : {a,b,c}) {",
      "                    edge_hash ^= value;",
      "                    edge_hash *= 1099511628211ULL;",
      "                }",
      "                for (int i : {a,b,c}) {",
      "                    for (int j : {a,b,c}) {",
      "                        for (int k : {a,b,c}) {",
      "                            if (i != j && i != k && j != k) {",
      "                                forbidden[i][j][k] = 1;",
      "                            }",
      "                        }",
      "                    }",
      "                }",
      "            }",
      "        }",
      "    }",
      "",
      "    const std::array<Point, 10> witness{{",
      "        {0,0},{0,1},{0,3},{0,4},{1,6},",
      "        {2,6},{5,5},{5,6},{6,3},{6,4}",
      "    }};",
      "    int checked = 0;",
      "    for (int a = 0; a < 10; ++a) {",
      "        for (int b = a + 1; b < 10; ++b) {",
      "            for (int c = b + 1; c < 10; ++c) {",
      "                const int x = distance2(witness[a],witness[b]);",
      "                const int y = distance2(witness[a],witness[c]);",
      "                const int z = distance2(witness[b],witness[c]);",
      "                if (x == y || x == z || y == z) return 2;",
      "                ++checked;",
      "            }",
      "        }",
      "    }",
      "    if (checked != 120 || edge_count != 2488",
      "        || edge_hash != 0xb36e0b83c873e23fULL) {",
      "        return 2;",
      "    }",
      "",
      "    const bool found = search(0,0);",
      "    const std::array<std::uint64_t, target + 1> expected_visits{",
      "        1,39,780,9035,59093,205914,353328,267906,84906,10035,448,0",
      "    };",
      "    const std::array<std::uint64_t, target + 1> expected_rejects{",
      "        0,0,1625,34375,280362,996123,1589251,1100072,318265,32717,1344,0",
      "    };",
      "    if (found || visits != expected_visits",
      "        || rejects != expected_rejects",
      "        || trace != 0x1ece71b42de90c50ULL) {",
      "        return 3;",
      "    }",
      "",
      "    std::uint64_t nodes = 0;",
      "    std::uint64_t rejected = 0;",
      "    for (auto value : visits) nodes += value;",
      "    for (auto value : rejects) rejected += value;",
      "    std::cout << \"witness 10 triples \" << checked << \" conflicts 0\\n\";",
      "    std::cout << \"hypergraph vertices 49 edges \" << edge_count",
      "              << \" fnv1a64 \" << std::hex << edge_hash << std::dec << \"\\n\";",
      "    std::cout << \"target 11 found 0 nodes \" << nodes",
      "              << \" rejects \" << rejected << \"\\n\";",
      "    std::cout << \"visits\";",
      "    for (auto 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://arxiv.org/abs/2411.00566",
    "locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R423",
      "title": "The exact maximum is I_7=10",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "no-isosceles-grid-7",
      "title": "no isosceles grid 7",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
no-isosceles-grid-7
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
arxiv.org ↗
Public record
R421
Stable alias
iso7-artifact-complete-eleven-search
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.