[baq]

Fascinating that you actually went through with an implementation. I’ve been throwing the idea of LLMs somehow having a sat solver built into them (maybe trained to have one as an emergent property), but something like you describe is the next best thing.