Date: Sun, 16 Oct 2022 11:38:01 -0400
From: Christopher Wellons <wellons@nullprogram.com>
To: Matthew Fernandez <matthew.fernandez@gmail.com>
Cc: ~skeeto/public-inbox@lists.sr.ht
Subject: Re: relationship to model checking
Message-ID: <20221016153801.fieqzt3ianrujnxd@nullprogram.com>
References: <725c9a46-6fd9-afcc-52de-268a3070eb5d@gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Disposition: inline
In-Reply-To: <725c9a46-6fd9-afcc-52de-268a3070eb5d@gmail.com>
User-Agent: NeoMutt/20170113 (1.7.2)

Thanks for the kind words, Matt! I've dabbled with Prolog, but otherwise 
I've never made use of constraint programming or model checkers. It's 
probably something I should learn, especially if I keep doing this. There 
is a growing number of interesting games from the book (Neutron, Order and 
Chaos, Splatter, Sequencium, Pennywise, Prophecies) that I'd like to 
explore more thoroughly. Do you have recommendations?

While working on Dandelions, I considered a multi-threaded tree search, 
but didn't feel it was worth building the machinery for it, particularly 
because it's ultimately memory constrained. (A branch exploration queue 
with appropriately-sized work chunks, synchronizing memoization, or 
per-thread memoization with even greater memory demands, etc.) Had it been 
pre-built as part of a model checker, I would have used it of course.

> I often wonder whether I myself could hand-write something that 
> outperforms it.

I wouldn't be surprised if a thoughtful, hand-written implementation 
outperforms the generated one, even if you've encoded as much knowledge as 
you can. There's likely still more context to be exploited. On the other 
hand, it sounds like it's already finely-tuned to this narrow problem 
space. Hard to say, especially since I'm not familiar with model checkers.

A couple months ago I showed it's easy to outperform "battle-hardened" 
generic hash tables in compiled languages (C++, Go, etc.) since you 
usually have so much local knowledge to exploit. I've had similar results 
parsing JSON and XML: With a known, fixed schema, a hand-written parser 
can be small and very, very fast vs. a generic parsing library. Here's my 
favorite talk on this subject:

Context is Everything
https://vimeo.com/644068002

Compared to a one-size-fits-all hash table or parser, the gap between 
generated vs. hand-written model checker is probably small. Also, if the 
goal is simply to prove some things about a game, it also probably doesn't 
matter whether you get the answer in 1 minute or 10 minutes. The main 
benefit would be speeding up testing and validation during development, 
after which it matters little. The performance boost could easily cost 
more than what you gain from faster testing (e.g. my decision not to 
bother with multi-threading).