Sophisticated sudokus as playful proof practice

Cracking the Cryptic quickly became my favorite pandemic past time. So much so that I've started making variant Sudokus - it's relaxing, creative, meditative, and I find it quite fun. I definitely second the suggestion to check out the CtC youtube channel!

And I encourage anyone with even a slight interest to check out the videos they post where constructors explain how they come up with some of the puzzles. I never imagined I'd be able to do it well or find it fun but I was pleasantly surprised after trying it out and having a blast.

The initial board is the starting axiom, and you want to prove (derive) a completely filled board. It's easier to think model-theoretically about games like this, but I've found that as I learn a logic puzzle over time, I build up a repertoire of rules I can apply. (In fact, for puzzles-masyu.com, I have a sound and mostly complete set of rules in my mind for the Medium difficulty and periodicals.)

The application of these rules typically produces a linear proof, because we augment the board state sequentially. But that's a human limitation, not a formal one. Since any rule that could be applied always can be applied (so long as there's a unique solution!), if you notice you can do two things from the same proof state, you can imagine a "rule of concurrency" that joins the results from multiple prior rules.

This kind of structure is even clearer in Picross 3D: Round Two, which has two different colors that interact very loosely. You can often work purely in one color, then switch to working on the other color, and go back and forth -- it's like you're interleaving two concurrent actors both collaborating on the same object. A purely semantic perspective doesn't really lend itself to this observation -- but when you've built up a corpus of rules, it's very obvious which rules are color-local and which require a more global view to progress.