| Bytes | Lang | Time | Link |
|---|---|---|---|
| 073 | Rust | 230822T163253Z | gsitcia |
| 006 | Wolfram Language Mathematica 13.0 | 230726T014222Z | 138 Aspe |
| 005 | Python 3 + PySAT | 230802T061921Z | alephalp |
| 005 | Python 3 + Z3 | 230802T000647Z | Bubbler |
| 005 | Wolfram Language Mathematica | 230725T104218Z | alephalp |
Rust, 8,7 in 3 minutes on the Rust playground
use std::time::Instant;
use std::{
collections::HashMap,
hash::Hash,
sync::atomic::{AtomicU32, Ordering},
};
use rayon::prelude::*;
const MAX_THREADS: usize = 4;
static NUM_TASKS: AtomicU32 = AtomicU32::new(0);
#[derive(Clone, Copy, Debug)]
struct Edge {
opposite_edge: u32,
opposite_color: u32,
opposite_vertex: u16,
}
#[repr(C)]
#[derive(Clone, Copy)]
struct Color {
up: u32,
down: u32,
vertex: u16,
last_edge: u32,
}
#[repr(C)]
#[derive(Clone, Copy)]
struct Vertex {
up: u32,
down: u32,
left: u16,
right: u16,
count_colors: u16,
count_edges: u16,
}
#[repr(C)]
#[derive(Clone, Copy)]
struct Root {
padding_1: u64,
left: u16,
right: u16,
padding_2: u32,
}
impl Root {
fn new() -> Self {
Self {
padding_1: 0,
left: 0,
right: 0,
padding_2: 0,
}
}
}
// the reason for repr(C) is so color/vertex up/down are in the same locations
#[repr(C, align(16))]
#[derive(Clone, Copy)]
union Node {
edge: Edge,
color: Color,
vertex: Vertex,
root: Root,
}
impl Default for Node {
fn default() -> Self {
Self { root: Root::new() }
}
}
#[derive(Clone)]
struct GraphColoring {
nodes: Vec<Node>,
allowance: u32,
// num_checks: u64,
max_colors: u32,
}
impl GraphColoring {
fn edge_mut(&mut self, idx: u32) -> &mut Edge {
unsafe { &mut self.nodes.get_mut(idx as usize).unwrap_unchecked().edge }
}
fn color_mut(&mut self, idx: u32) -> &mut Color {
unsafe { &mut self.nodes.get_mut(idx as usize).unwrap_unchecked().color }
}
fn vertex_mut(&mut self, idx: u16) -> &mut Vertex {
unsafe { &mut self.nodes.get_mut(idx as usize).unwrap_unchecked().vertex }
}
fn edge(&self, idx: u32) -> Edge {
unsafe { self.nodes.get(idx as usize).unwrap_unchecked().edge }
}
fn color(&self, idx: u32) -> Color {
unsafe { self.nodes.get(idx as usize).unwrap_unchecked().color }
}
fn vertex(&self, idx: u16) -> Vertex {
unsafe { self.nodes.get(idx as usize).unwrap_unchecked().vertex }
}
fn pick_min_vertex(&self) -> Option<(u16, u16)> {
let mut idx = self.vertex(0).right;
if idx == 0 {
return None;
}
let mut fewest_colors = self.max_colors as _;
let mut most_edges = 0;
let mut bestidx = idx;
loop {
let vertex = self.vertex(idx);
if vertex.count_colors < fewest_colors
|| (vertex.count_colors == fewest_colors && vertex.count_edges > most_edges)
{
if vertex.count_colors == 0 {
return Some((0, 0));
}
if vertex.count_colors == 1 {
return Some((idx, 1));
}
fewest_colors = vertex.count_colors;
most_edges = vertex.count_edges;
bestidx = idx;
}
idx = vertex.right;
if idx == 0 {
break;
}
}
Some((bestidx, fewest_colors))
}
fn disconnect_color(&mut self, color_idx: u32, color: Color) {
for idx in color_idx + 1..=color.last_edge {
let edge = self.edge(idx);
let opposite_edge_idx = edge.opposite_edge;
let opposite_color_idx = edge.opposite_color;
let opposite_color = self.color(opposite_color_idx);
debug_assert!(opposite_edge_idx <= opposite_color.last_edge);
debug_assert!(opposite_edge_idx >= opposite_color_idx);
if opposite_edge_idx < opposite_color.last_edge {
// swap nodes at opposite_edge_idx and opposite_color.last_edge
// that means our pointer has to change, as well as last_edges oppoosite_edge has to change
let last_edge_idx = opposite_color.last_edge;
let last_edge = self.edge(last_edge_idx);
let last_edge_opposite_idx = last_edge.opposite_edge;
self.edge_mut(last_edge_opposite_idx).opposite_edge = opposite_edge_idx;
*self.edge_mut(opposite_edge_idx) = Edge {
opposite_edge: last_edge_opposite_idx,
opposite_color: last_edge.opposite_color,
opposite_vertex: last_edge.opposite_vertex,
};
*self.edge_mut(last_edge_idx) = Edge {
opposite_edge: idx,
opposite_color: color_idx,
opposite_vertex: color.vertex,
};
// self.edge_mut(last_edge_idx).opposite_edge = idx;
// self.edge_mut(last_edge_idx).opposite_color = color_idx;
self.edge_mut(idx).opposite_edge = last_edge_idx;
}
self.color_mut(opposite_color_idx).last_edge -= 1;
self.vertex_mut(opposite_color.vertex).count_edges -= 1;
debug_assert_eq!(
self.edge(idx).opposite_edge,
self.color(edge.opposite_color).last_edge + 1
);
}
}
fn reconnect_color(&mut self, color_idx: u32, color: Color) {
for edge_idx in (color_idx + 1..=color.last_edge).rev() {
let edge = self.edge(edge_idx);
debug_assert_eq!(
edge.opposite_edge,
self.color(edge.opposite_color).last_edge + 1
);
self.color_mut(edge.opposite_color).last_edge += 1;
let color = self.color(edge.opposite_color);
self.vertex_mut(color.vertex).count_edges += 1;
}
}
#[inline]
fn remove_adjacent(&mut self, color_idx: u32, color: Color) {
for edge_idx in (color_idx + 1..=color.last_edge).rev() {
let edge = self.edge(edge_idx);
let color1_idx = edge.opposite_color;
let color1 = self.color(color1_idx);
self.disconnect_color(color1_idx, color1);
self.color_mut(color1.up).down = color1.down;
self.color_mut(color1.down).up = color1.up;
let vertex = self.vertex_mut(color1.vertex);
vertex.count_colors -= 1;
vertex.count_edges -= (color1.last_edge - color1_idx) as u16;
}
}
fn reconnect_adjacent(&mut self, color_idx: u32, color: Color) {
for edge_idx in color_idx + 1..=color.last_edge {
let edge = self.edge(edge_idx);
let color1_idx = edge.opposite_color;
let color1 = self.color(color1_idx);
self.reconnect_color(color1_idx, color1);
self.color_mut(color1.up).down = color1_idx;
self.color_mut(color1.down).up = color1_idx;
let vertex = self.vertex_mut(color1.vertex);
vertex.count_colors += 1;
vertex.count_edges += (color1.last_edge - color1_idx) as u16;
}
}
fn check(&mut self) -> bool {
let (vertex_idx, count) = match self.pick_min_vertex() {
None => {
return true;
}
Some(x) => x,
};
if count == 0 {
return false;
}
// self.num_checks += 1;
let vertex_idx = vertex_idx as u32;
let mut idx = self.color(vertex_idx).down;
while idx != vertex_idx {
let color = self.color(idx);
self.disconnect_color(idx, color);
idx = color.down;
}
let mut allowance = count as u32 - self.allowance;
let vertex = self.vertex(vertex_idx as _);
self.vertex_mut(vertex.left).right = vertex.right;
self.vertex_mut(vertex.right).left = vertex.left;
idx = vertex.down;
let has_allowance = self.allowance > 0;
let x = count as u32 - self.allowance.saturating_sub(1);
let num_tasks = NUM_TASKS.load(Ordering::Relaxed);
let parallel = num_tasks < MAX_THREADS as u32
&& NUM_TASKS
.compare_exchange_weak(
num_tasks,
num_tasks + x - 1,
Ordering::SeqCst,
Ordering::Relaxed,
)
.is_ok();
if parallel {
let mut tasks = Vec::new();
while idx != vertex_idx {
let color = self.color(idx);
if has_allowance && allowance == 0 {
self.allowance -= 1;
}
if (idx + 1..=color.last_edge).all(|edge_idx| {
self.vertex(self.edge(edge_idx).opposite_vertex)
.count_colors
> 1
}) {
self.remove_adjacent(idx, color);
tasks.push(self.clone());
self.reconnect_adjacent(idx, color);
}
if has_allowance && allowance == 0 {
self.allowance += 1;
break;
}
idx = self.color(idx).down;
allowance -= 1;
}
idx = self.color(vertex_idx).up;
while idx != vertex_idx {
let color = self.color(idx);
self.reconnect_color(idx, color);
idx = color.up;
}
self.vertex_mut(vertex.left).right = vertex_idx as _;
self.vertex_mut(vertex.right).left = vertex_idx as _;
let o = tasks.par_drain(..).any(|mut i| i.check());
NUM_TASKS.fetch_sub(x - 1, Ordering::Relaxed);
o
} else {
while idx != vertex_idx {
let color = self.color(idx);
if has_allowance && allowance == 0 {
self.allowance -= 1;
}
if (idx + 1..=color.last_edge).all(|edge_idx| {
self.vertex(self.edge(edge_idx).opposite_vertex)
.count_colors
> 1
}) {
self.remove_adjacent(idx, color);
if self.check() {
return true;
}
self.reconnect_adjacent(idx, color);
}
if has_allowance && allowance == 0 {
self.allowance += 1;
break;
}
idx = self.color(idx).down;
allowance -= 1;
}
idx = self.color(vertex_idx).up;
while idx != vertex_idx {
let color = self.color(idx);
self.reconnect_color(idx, color);
idx = color.up;
}
self.vertex_mut(vertex.left).right = vertex_idx as _;
self.vertex_mut(vertex.right).left = vertex_idx as _;
false
}
}
fn new<T, F>(vertices: &Vec<T>, adjacent: F, max_colors: u32) -> GraphColoring
where
F: Fn(T, T) -> bool,
T: Hash + Eq + Copy,
{
let mut this = GraphColoring {
nodes: vec![Node::default()],
allowance: max_colors,
// num_checks: 0,
max_colors,
};
let mut vertex_idxs = HashMap::new();
// add vertex nodes
for &v in vertices {
let vertex_idx = this.nodes.len() as u16;
let left_idx = vertex_idx - 1;
let right_idx = 0;
let vertex = Vertex {
up: vertex_idx as _,
down: vertex_idx as _,
left: left_idx,
right: right_idx,
count_colors: 0,
count_edges: 0,
};
vertex_idxs.insert(v, vertex_idx);
this.nodes.push(Node { vertex });
this.vertex_mut(left_idx).right = vertex_idx;
this.vertex_mut(right_idx).left = vertex_idx;
}
let mut edge_to_idx = HashMap::new();
// add colors
for &a in vertices {
let vertex_a_idx = vertex_idxs[&a];
for k in 0..max_colors {
let color_a_idx = this.nodes.len() as _;
let up_idx = this.vertex(vertex_a_idx).up;
let down_idx = vertex_a_idx as _;
let color_a = Color {
up: up_idx,
down: down_idx,
vertex: vertex_a_idx,
last_edge: color_a_idx,
};
this.nodes.push(Node { color: color_a });
this.color_mut(up_idx).down = color_a_idx;
this.color_mut(down_idx).up = color_a_idx;
this.vertex_mut(vertex_a_idx).count_colors += 1;
// and edges
for &b in vertices {
if a == b {
continue;
}
if adjacent(a, b) {
let edge_a_idx = this.nodes.len() as _;
let edge_a = match edge_to_idx.get(&(b, a, k)) {
Some(&(edge_b_idx, color_b_idx, vertex_b_idx)) => {
this.edge_mut(edge_b_idx).opposite_color = color_a_idx;
this.edge_mut(edge_b_idx).opposite_edge = edge_a_idx;
this.edge_mut(edge_b_idx).opposite_vertex = vertex_a_idx;
Node {
edge: Edge {
opposite_color: color_b_idx,
opposite_edge: edge_b_idx,
opposite_vertex: vertex_b_idx,
},
}
}
None => {
edge_to_idx
.insert((a, b, k), (edge_a_idx, color_a_idx, vertex_a_idx));
Node::default()
}
};
this.nodes.push(edge_a);
this.color_mut(color_a_idx).last_edge = edge_a_idx;
this.vertex_mut(vertex_a_idx).count_edges += 1;
}
}
}
}
this
}
fn chromatic_number(n: u32, d: u32, max_colors: u32) -> bool {
if d % 2 == 1 {
return max_colors >= 2;
}
let mut g = GraphColoring::new(
&(0_u32..1 << n)
.filter(|&i| i.count_ones() % 2 == 0)
.collect(),
|a, b| (a ^ b).count_ones() == d,
max_colors,
);
let out = g.check();
// println!("Num checks: {}", g.num_checks);
out
}
}
fn chromatic(n: u32, d: u32) -> u32 {
for k in 2.. {
if GraphColoring::chromatic_number(n, d, k) {
return k;
}
}
panic!("You're never gonna reach this");
}
fn main() {
let start = Instant::now();
rayon::ThreadPoolBuilder::new()
.num_threads(MAX_THREADS)
.build_global()
.unwrap();
for n in 2..=8 {
for d in 1..n {
println!("{},{} -> {}", n, d, chromatic(n, d));
}
}
println!("Finished in: {:?}", start.elapsed());
}
Formulates the decision problem as an exact cover problem and then uses dancing links to solve it.
Specifically, rows correspond to coloring a vertex a color. The columns correspond to the conditions that each vertex is covered by exactly one color, and that each edge has at most one vertex for any given color.
There are two graph coloring specific optimizations:
Colors are chosen in order. That is, when choosing the color for a vertex, only one of the colors that haven't yet been chosen must be considered. Without this optimization, proving that
f(8,6)is not5takes 415 million steps, with the optimization it takes around 1 million steps (and it's presumably even more effective for proving the chromatic number is not 6, since it's pruning more colors in that case).Ties are broken by finding the vertex with the maximum number of unassigned neighbors. This is also a pretty good optimization, without it (but with the previous) 4,225,666,594 steps are required to prove the chromatic number is not 6, with it only 299,285,005 steps are necessary.
If you run it on your own computer, make sure to run cargo add rayon and compile with the RUSTFLAGS=-Ctarget-cpu=native environment variable.
Wolfram Language (Mathematica 13.0), 392 bytes, 11,6 in a minute on my laptop
Just implementation.
Use VertexChromaticNumber instead of IGraphM`IGChromaticNumber to get vertex-chromatic number, \$ \color{red}{\text{some results are not correct.}} \$
GetChromaticNumber[n_, d_] :=
Module[{nodes, edges, g}, nodes = Tuples[{0, 1}, n];
edges =
Select[Subsets[nodes, {2}], HammingDistance[#[[1]], #[[2]]] == d &];
g = Graph[UndirectedEdge @@@ edges];
VertexChromaticNumber[g]]
(*To use the function,enter the two integers as arguments.For \
example:*)
Do[Print[{n, d} -> GetChromaticNumber[n, d]], {n, 2, Infinity}, {d, 1,
n - 1}]
\$ \begin{array}{c|ccccccccccc} n\backslash d & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 \\ \hline 2 & 2 & - & - & - & - & - & - & - & - & - \\ 3 & 2 & 4 & - & - & - & - & - & - & - & - \\ 4 & 2 & 4 & 2 & - & - & - & - & - & - & - \\ 5 & 2 & 8 & 2 & 4 & - & - & - & - & - & - \\ 6 & 2 & 8 & 2 & 7 & 2 & - & - & - & - & - \\ 7 & 2 & 8 & 2 & 8 & 2 & 4 & - & - & - & - \\ 8 & 2 & 8 & 2 & 8 & 2 & 7 & 2 & - & - & - \\ 9 & 2 & 15❌ & 2 & 16 & 2 & 11 & 2 & 4 & - & - \\ 10 & 2 & 17❌ & 2 & 33 & 2 & 20 & 2 & 7 & 2 & - \\ 11 & 2 & 19❌ & 2 & 56 & 2 & 35 & 2 & 12 & 2 & 4 \\ \end{array} \$
VertexChromaticNumber function was Introduced in 13 (13.0)
Whereas TIO Mathematica version is 12.0.1
Print["Mathematica version: ", $Version];
Print["Operating system: ", $OperatingSystem];
Mathematica version: 12.0.1 for Linux x86 (64-bit) (October 16, 2019)
Operating system: Unix
Python 3 + PySAT, 8,5
from pysat.solvers import Cadical153 as Solver
from pysat.card import CardEnc
from pysat.formula import IDPool
import time
chromatic_dict = {}
def colorable(n, d, k):
s = Solver()
pool = IDPool(start_from=(k << n) + 1)
for i in range(1 << n):
cnf = CardEnc.equals(lits=[(i * k) + l + 1 for l in range(k)], vpool=pool)
s.append_formula(cnf.clauses)
for i in range(1 << n):
for j in range(i + 1, 1 << n):
if (i ^ j).bit_count() == d:
for l in range(k):
s.add_clause([-(i * k) - l - 1, -(j * k) - l - 1])
return s.solve()
def chromatic(n, d):
if (n - 1, d) in chromatic_dict:
k = chromatic_dict[(n - 1, d)]
else:
k = 1
while not colorable(n, d, k):
k += 1
chromatic_dict[(n, d)] = k
return k
if __name__ == "__main__":
n = 1
start_time = time.time()
while True:
n += 1
for d in range(1, n):
chromatic_number = chromatic(n, d)
time_elapsed = time.time() - start_time
print(f"[{time_elapsed}] {n},{d} -> {chromatic_number}")
A port of My Mathemactica answer, using PySAT with CaDiCaL SAT solver.
Python 3 + Z3, 8,5
import z3
def check(nodes, d, limit):
solver = z3.SolverFor('QF_FD')
for node in nodes:
solver.add(1 <= node, node <= limit)
l = len(nodes)
for i in range(l):
for j in range(l):
cnt = bin(i ^ j).count('1')
if d-1 <= cnt <= d:
solver.add(nodes[i] != nodes[j])
return solver.check() == z3.sat
def solve(n, d, lower=1):
if d % 2: return 2
nodes = [z3.Int(f'a{i}') for i in range(2**(n-1))]
upper = (lower + 1) * 2
while lower + 1 < upper:
mid = lower + 1
if mid == lower: mid += 1
result = check(nodes, d, mid)
print(n, d, mid, result)
if result: upper = mid
else: lower = mid
return upper
def main():
from time import time
start = time()
n = 2
memo = [[0], [0]]
while True:
memo.append([0])
for d in range(1, n):
if d + 1 < n: sol = solve(n, d, memo[n-1][d] - 1)
else: sol = solve(n, d)
print(n, d, '->', sol, '( elapsed:', time() - start, ')')
memo[n].append(sol)
n += 1
main()
Output:
2 1 -> 2 ( elapsed: 5.245208740234375e-06 )
3 1 -> 2 ( elapsed: 6.246566772460938e-05 )
3 2 2 False
3 2 3 False
3 2 -> 4 ( elapsed: 0.012233257293701172 )
4 1 -> 2 ( elapsed: 0.012252330780029297 )
4 2 4 True
4 2 -> 4 ( elapsed: 0.019064903259277344 )
4 3 -> 2 ( elapsed: 0.01909017562866211 )
5 1 -> 2 ( elapsed: 0.01910543441772461 )
5 2 4 False
5 2 5 False
5 2 6 False
5 2 7 False
5 2 -> 8 ( elapsed: 6.083156585693359 )
5 3 -> 2 ( elapsed: 6.083175420761108 )
5 4 2 False
5 4 3 False
5 4 -> 4 ( elapsed: 6.109014987945557 )
6 1 -> 2 ( elapsed: 6.109039783477783 )
6 2 8 True
6 2 -> 8 ( elapsed: 6.180561542510986 )
6 3 -> 2 ( elapsed: 6.180585145950317 )
6 4 4 False
6 4 5 False
6 4 6 False
6 4 7 True
6 4 -> 7 ( elapsed: 34.04813623428345 )
6 5 -> 2 ( elapsed: 34.048160791397095 )
7 1 -> 2 ( elapsed: 34.04817223548889 )
7 2 8 True
7 2 -> 8 ( elapsed: 34.29183101654053 )
7 3 -> 2 ( elapsed: 34.29185700416565 )
7 4 7 False
7 4 8 True
7 4 -> 8 ( elapsed: 35.03852438926697 )
7 5 -> 2 ( elapsed: 35.0385627746582 )
7 6 2 False
7 6 3 False
7 6 -> 4 ( elapsed: 35.16324186325073 )
8 1 -> 2 ( elapsed: 35.1632719039917 )
8 2 8 True
8 2 -> 8 ( elapsed: 35.805861949920654 )
8 3 -> 2 ( elapsed: 35.80588483810425 )
8 4 8 True
8 4 -> 8 ( elapsed: 37.375497817993164 )
8 5 -> 2 ( elapsed: 37.37552309036255 )
8 6 4 False
Looking at the timing, there were a couple of points where Z3 struggled badly:
- ~5 seconds to prove
5,2is not7-colorable - ~30 seconds to prove
6,4is not6-colorable - ?? seconds to prove
8,6is not5-colorable- Given that the answer is 7, it will require a major breakthrough to beat
8,6in a minute. I'm pretty confident that naively plugging the graph into any SAT/SMT solver won't cut it.
- Given that the answer is 7, it will require a major breakthrough to beat
Initially I tried binary search on the number of colors, but I realized that Z3 takes a pretty long time to provide a k-coloring when k is larger than optimal, so I replaced it with a sequential search from the lower bound. The lower bound is the same as alephalpha's:
memoizes the result for
f[n,d]as a lower bound forf[n+1,d].
An additional contribution of this answer is that, for even d, the graph has two connected components that are isomorphic, so we only need to compute the answer on one of them.
Proof:
- If
dis even, this meansaandbhave equal parity (in terms of the number of ones), i.e. there is no path from an even node to an odd node and vice versa. Also, sinced < n, there is always a way to flip two bits of a node in two steps (e.g.10111...and then01111...), so the graph has exactly two connected components. - "Hamming distance of
aandbisd" is the same as "a^bhasdones". Assumeaandbare even. Then the two are connected iff (if and only if)a^bhasdones. Now consider two odd nodesa^1andb^1. These two are connected iff(a^1)^(b^1) == a^bhasdones. The same holds whenaandbare odd, so the two connected components have an isomorphism ofa <=> a^1.
The single connected component can be constructed with the rule of "there is an edge between a and b iff a^b has d or d-1 ones". Proof:
- Take the connected component of even nodes from the original graph. We can remove the least significant bit from all nodes to get the labels of 0 to
2**(n-1). The removed bit is the parity of the rest; I will call it the parity bit. - Given the two nodes
aandbin the original space, "a^bhasdones" has two possibilities:aandbhave the same parity bit:(a/2)^(b/2)hasdones.aandbhave different parity bit:(a/2)^(b/2)hasd-1ones.
- The converse is also true:
(a/2)^(b/2)must havedord-1ones; otherwisea^bcannot havedones.- if
(a/2)^(b/2)hasdones,a/2andb/2have the same parity, soa^bhasdones. - if
(a/2)^(b/2)hasd-1ones,a/2andb/2have different parity, soa^bhasdones.
Also, I have set the upper bound to be lower_bound * 2 (where the lower bound is f(n-1,d)), so in some cases the code skips one calculation when the graph is not upper_bound - 1-colorable. Proof:
- The graph for
n,dequals two disjoint copies of that ofn-1,dplus extra edges in between. The nodes ofn,dcan be split by their first bit, and observe the follows:0{a} ^ 0{b}(whereaandbcontainsn-1bits each) hasdord-1ones iff{a} ^ {b}does. The same holds when 0 is replaced with 1.- Therefore, the induced subgraph of
n,dby selecting all nodes with the first bit of 0 (or 1) isf(n-1,d)-colorable.
- Take a coloring of
n-1,dusingkcolors. There exists an2k-coloring ofn,d: Color the first half using colors1tok. Color the rest using colorsk+1to2k.
Wolfram Language (Mathematica), 370 bytes, 8,5 in a minute on TIO
f[n_, d_] :=
f[n, d] =
Block[{c, k}, k = If[n < d + 1, 1, f[n - 1, d]];
While[! SatisfiableQ[
Array[BooleanCountingFunction[{1}, Table[c[#, i], {i, k}],
"CNF"] &, 2^n, 0, And] &&
Array[If[
DigitCount[BitXor[#, #2], 2, 1] ==
d, ! c[#, #3] || ! c[#2, #3], True] &, {2^n, 2^n, k}, {0,
0, 1}, And]], k++]; k]
Uses Mathematica's built-in SAT solver, and memoizes the result for f[n,d] as a lower bound for f[n+1,d].