Largest binary rectangle without any arithmetic progressions

What is the largest rectangular grid (by area) that you can color in red and blue such that there is no red cell halfway between two red cells and no blue cell halfway between two blue cells, moving in a straight line horizontally or vertically?

Bonus question: what happens if we also include the $$\pm 1$$ diagonal lines?

Just horizontal and vertical:

8x8:

Optimal because 9 in one direction is impossible.

Horizontal, vertical, and +-1 slope diagonal:

8x4:

Discovered to be optimal using a SAT solver. In particular, 5x5 is impossible.

I proved optimality for the latter solution using a SAT solver. Here's the Rust code I used to generate the CNF file:

use std::env;
use std::fs::File;
use std::io::Write;

type Point = (usize, usize);
fn main() -> std::io::Result<()> {
let mut args = env::args();
let _ = args.next();
let x_size: usize = args.next().expect("X arg").parse().expect("X num");
let y_size: usize = args.next().expect("Y arg").parse().expect("Y num");
let filename = format!("grid-{}{}.cnf", x_size, y_size);
let mut file = File::create(&filename)?;
let points: Vec<Point> = (0..x_size)
.flat_map(|i| (0..y_size).map(move |j| (i, j)))
.collect();
let to_var = &|i, j| i + j * x_size + 1;
let mut count = 0;
for &(i, j) in &points {
for &(k, l) in &points {
if (i + k) % 2 == 0 && (j + l) % 2 == 0 && (i, j) < (k, l) {
if i == k || j == l || (j < l && k - i == l - j) || (j > l && k - i == j - l) {
count += 2;
}
}
}
}
writeln!(&mut file, "p cnf {} {}", x_size * y_size, count)?;
for &(i, j) in &points {
for &(k, l) in &points {
if (i + k) % 2 == 0 && (j + l) % 2 == 0 && (i, j) < (k, l) {
if i == k || j == l || (j < l && k - i == l - j) || (j > l && k - i == j - l) {
let mid1 = (i + k) / 2;
let mid2 = (j + l) / 2;
let v1 = to_var(i, j);
let v2 = to_var(mid1, mid2);
let v3 = to_var(k, l);
writeln!(&mut file, "{} {} {} 0", v1, v2, v3)?;
writeln!(&mut file, "-{} -{} -{} 0", v1, v2, v3)?;
}
}
}
}
println!("{}", filename);
Ok(())
}

• Fascinating that they are so regular! Commented Jul 11, 2023 at 10:43
• You get another solution if you shift by one column
– daw
Commented Jul 11, 2023 at 11:19
• @daw do you mean shift everything? this is obvious, but you can also swap red and blue. Commented Jul 11, 2023 at 13:07

Some logic to arrive at the solution

The rule is: No Same colored cell half way between to cells. So we can rule out a lot of patterns. We are only looking at horizontal patterns in the first step and will expand it to vertical patterns after that.

Forbidden patterns (using X/O for better readability):

 - XXX     there can never be 3 same colored squares
- X_X_X   for five squares (the middle square has to be different)
- X__X__X for seven squares


So we can start with 3 squares and simply extend the line with all possible combinations (we're ignoring inverted solutions):

 3: 00X                    0X0                              X00
4: 00X0           00XX    0X00            0X0X             X00X
5: 00X00   00X0X  00XX0   0X00X           0X0XX            X00X0         X00XX
6: 00X00X  00X0XX 00XX00  00XX0X          0X0XX0           X00X00 X00X0X X00XX0
7: 00X00XX        00XX00X 00XX0X0 00XX0XX 0X0XX00  0X0XX0X               X00XX00
8:                00XX00XX                         0X0XX0X0              X00XX00X
9: -


Since we cannot find an extension for any of the 8-square patterns, the maximum solution is 8x8.

Now we just have to identify which lines can be combined, so the vertical lines also follow one of the patterns. Since we can just invert the pattern on each other line, we can combine these 3 patterns to a total of 3x3=9 solutions, if we also count the inverted colors a total of 18 solutions.

 Basic pattern      shifted            Mixed pattern    ...
0 0 X X 0 0 X X    0 X X 0 0 X X 0    0 X 0 X X 0 X 0
0 0 X X 0 0 X X    X 0 0 X X 0 0 X    0 X 0 X X 0 X 0
X X 0 0 X X 0 0    X 0 0 X X 0 0 X    X 0 X 0 0 X 0 X
X X 0 0 X X 0 0    0 X X 0 0 X X 0    X 0 X 0 0 X 0 X
0 0 X X 0 0 X X    0 X X 0 0 X X 0    0 X 0 X X 0 X 0
0 0 X X 0 0 X X    X 0 0 X X 0 0 X    0 X 0 X X 0 X 0
X X 0 0 X X 0 0    X 0 0 X X 0 0 X    X 0 X 0 0 X 0 X
X X 0 0 X X 0 0    0 X X 0 0 X X 0    X 0 X 0 0 X 0 X