Alright, Z3 took ~16 seconds on the purely-SAT encoding of the problem
Which makes me wonder: can we have some kind of lowering/optimisation pass on SMT problems, and lower them to an equivalent SAT if possible? Or is that just left as an exercise to the developer :p

Have not yet gone back and tried a pure-SAT encoding with Z3 to see how fast that is
Curious if any SMT/SAT whisperers know more about this. I continue to be amazed at these things

The runtime? ~5 seconds. Over a thousand times faster
Unfortunately, it's looking like 9x9 may still be a bridge too far 🙃

But more complicated shapes are gonna be pretty niche/technical, so I wouldn't trust my cursory search to get a definitive answer to how they're done

fwiw, I took an intro to ASL class earlier this year, and we only did 2D shapes, but they were all "make the shape with your hands in the air"
Looking online, 3D shapes seem to be some combination of "make the shape" and occasionally signing the number of faces to disambiguate

Also a middle ground b/w "give up negotiations a couple days before SNAP funds for November are forcibly sent out" and "12-months of famine"

I think it would be less insulting if there wasn't even the fig leaf for a vote on ACA premiums, and the Dems just admitted that there were other factors in their reversal

void return type for main? heresy!

This is probably an actually useful thing to have, I just think it's funny that Chrome is in a huff over the passwords submitted in my plain-text connection to localhost

Found a 9x9 one after an hour or so (works better rendered in monospace 😅):

4 8 3 2 5 7 9 1 6
1 2 5 7 8 6 3 4 9
2 5 8 4 7 9 1 6 3
8 3 7 1 6 4 5 9 2
5 6 4 8 9 2 7 3 1
3 4 9 6 2 1 8 5 7
7 9 1 3 4 5 6 2 8
6 1 2 9 3 8 4 7 5
9 7 6 5 1 3 2 8 4

I found this using an SMT solver (took a few minutes to run). It would be cool to see how much farther you can take it

What's interesting about it is: Exactly 1 pair of 1's are a knight's move apart (two spaces apart in one axis, one space apart in the other). Exactly 2 pairs of 2's are. And so on, up to exactly 8 pairs of 8's are a knight's move apart (look at how the 8's cluster on a diagonal)

> small model
> 357B
(._.)

Also if you look at the original logo, my mountains are pretty simplified. I took one look and decided that I'd rather not go for dozens of tiny lines 😅

split the difference like Solomon and cut each king in half

this was Boston Common, and any shot I took could not capture the number of people there