SAT solvers and the algorithms surrounding them are so much fun. I agree they are very unappreciated.
Shameless plug: I wrote a (admittedly very deriative) introduction with some examples I thought at the time were cool.
SMT is so much fun. The Z3 Python api lets you write your problem very directly and then gives you fast answers, even for quite large problems.
I tried to write a programming language that compiles to SAT many years ago: https://sentient-lang.org/
Some additional context: Outside of Microsoft, this puzzle is often known as Star Battle.
Terrific little puzzle, highly recommend it!
How good are current LLMs at translating problems given as text into something SMT solvers can operate on? Be it MiniZinc, Z3, Smtlib, Python bindings, etc. Anyone tried it out?
Haha, Marijn Heule who is pushing a lot of limits of SAT solving would love this. If you manage to get him excited, he might spend a few years on this problem :) He's kinda famous for solving the Boolean Pythagorean Triples problem using SAT [1]. He loves puzzles. He also got Knuth excited about a bunch of fun puzzles.
BTW, these puzzles also tend to have a lot of symmetries, which SAT solvers are pretty bad at handling. You can break them, though, using a variety of techniques, e.g. static symmetry breaking [2], or symmetric learning.
[1] https://www.cs.utexas.edu/~marijn/ptn/ [2] https://github.com/markusa4/satsuma
If you want a language for expressing constraint satisfaction problems that's higher-level than SAT, I think MiniZinc is pretty interesting. https://www.minizinc.org/
Reminds me of a small project I did back in undergrad: Minesweeper using a SMT solver. https://github.com/stong/smt-minesweeper
I actually wrote a backtracking solution to the LinkedIn queens game a while ago (and the tango game).
I know nothing about SMT or SAT and I imagine they might be faster, but the backtracking appears to solve just as instantaneously when you push the button.
Might be cool to learn a bit about SMT or SAT. Not sure how broadly applicable they are but I've seen people use them to solve some difficult advent of code problems if nothing else.
Hah, about a month ago I wrote a DLX solver for exact cover problems and LiQueens was one of my first implementations.
Next I want to try to solve the Tango and Zip games.
> Which is the correct solution to the queens puzzle. I didn't benchmark the solution times, but I imagine it's considerably slower than a raw SAT solver. Glucose is really, really fast.
I'm new to this area, neither the original article nor the link to Glucose have enough info to tell me order of magnitude here: milliseconds? hours?
you mentioned SMT is slower than SAT and left it there, but that feels incomplete. in problems like this, solve time barely matters unless you’re generating at scale. the real weight is in how fast you can write, refactor, and trust the constraints. SAT might give faster outputs, but SMT usually gets you to correct models quicker with less friction. wondering if you actually benchmarked both and stuck with SAT on numbers, or if it was more of a default comfort pick. felt like a missed moment to shift the lens from solver speed to model dev loop speed
I was briefly looking into using SMT for Minecraft autocrafting, but it turns out you can do integer linear programming and the mapping is easier.
What about a CP solver?
The article fails to even say what SMT is. It also fails to describe and explain it. This article should help:
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
Formal Methods in general are underrated in the industry. Pretty much no large companies except AWS (thank you Byron Cook!) use them at a large scale.
Edit: maybe there are large companies that use them behind the curtains, but AWS is the only place I know of where they publicly acknowledge how much they appreciate and use formal methods. If you know any of them, please comment and I'd be curious to learn about how they're using it!