Solving LinkedIn Queens with SMT
buttondown.com
buttondown.com
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!
At least Microsoft and Google poured a lot of money into this by funding well-staffed multi-year research projects. There's plenty of public trail in terms of research papers. It's just that not a whole lot came out of it otherwise.
The problem isn't that the methods are underrated, it's that they aren't compatible with the approach to software engineering in these places (huge monolithic codebases, a variety of evolving languages and frameworks, no rigid constraints on design principles).
Contrast with
Testing = “My tests prove these inputs definitely produce these test outputs”
IME Formal methods struggle making contact with reality because you really only get their promise “it always does what it is constrained to do” when every abstraction underneath provides the same guarantee, I wager most CPUs/GPUs aren’t verified down to the gate level these days.
It’s just faster to “trust” tests with most of the benefit, and developing software faster is very important to capturing a market and accruing revenue if you are building your software for business reasons.
EDIT: My gate-level verification remark is a bit extreme, but it applies to higher layers of the stack. The linux kernel isn’t verified. Drivers are sometimes verified, but not often. There is an HN comment somewhere about building a filesystem in Coq, and while the operations at the filesystem layer are provably correct, the kernel interfaces still fail. The firmware still isn’t proven. The CPU itself running on has undisclosed optimizations in its caches and load/store mechanisms which just aren’t proven, but enabled it to beat the competition on benchmarks, driving sales.
For the vast majority of software though they don't really make much sense because formally verifying the software is 10-100x more work than writing it and testing it with normal methods. And formal verification of software generally requires faaaaar more expertise than most people have. (The situation is much better for hardware design because it tends to be way simpler.)
It's a very powerful tool but also extremely difficult to use.
I don't think that's true at all. I suppose that depends on what you mean by formal methods and in what context you're concerned about those. Off the top of my head this comes to mind from Microsoft: https://learn.microsoft.com/en-us/windows-hardware/drivers/d...
Just for some quick examples:
Microsoft: https://github.com/Azure/azure-cosmos-tla, https://www.youtube.com/watch?v=kYX6UrY_ooA
Google: https://research.google/pubs/specifying-bgp-using-tla/, https://www.researchgate.net/publication/267120559_Formal_Mo...
Oracle: https://blogs.oracle.com/cloud-infrastructure/post/sleeping-... (note the author is a "Formal Verification Engineer", it's literally his job at Oracle to do this stuff)
Intel: https://dl.acm.org/doi/10.1145/1391469.1391675, https://link.springer.com/chapter/10.1007/978-3-540-69850-0_...
Jetbrains: https://lp.jetbrains.com/research/hott-and-dependent-types/
I'd also probably would count MS Research against that, or separately, since they're more like a University lab than a business. Labs often can run at a loss doing research on things that might not be practical. MS Research certainly has produced some practical things. Yet, what they do wont likely apply to a random, for-profit company.
Very, very, few companies find this stuff practical outside hardware companies where it's easier to apply with clearer ROI. There's also uptake in both cryptocurrency space and distributed databases. Most business software won't use it because it makes no sense to.
Shameless plug: I wrote a (admittedly very deriative) introduction with some examples I thought at the time were cool.
https://gist.github.com/enigma/98ea0392471fa70211251daa16ce8...
Terrific little puzzle, highly recommend it!
I try not to use them too much because I want to build the skill of using SMTs directly for now.
Besides which, I would argue the process of writing proof in the language is integral to building the understanding you need to deal with the results. You'll spot bugs as you're creating the model.
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
board =: 3 : '? (y,y) $ y'
test =: 4 : 0
m =. x
n =. #x
n -: # ~. ({&m) <"1 (i. n) ,. 0 A. (i. n)
)
findsol =:3 : 0
ns =. 1 i.~ (y & test)"0 i. !#y
if. (ns = !#y) do. 'No solution found'
else.
ns A. i. #y
end.
)
m =: board 5
m
4 4 0 1 1
3 2 0 1 1
2 4 1 1 0
3 2 1 3 4
2 0 2 2 0
0 1 2 3 4
findsol m
0 1 2 3 4
echo 'So the solution found is putting the queens in the diagonal'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.
NP-complete are the hardest problems in NP. Cook in 1971 proved SAT to be in NP-complete. In the worst case for any other problem in NP, we can quickly (i.e., in polynomial time) convert instances of that problem into instances of SAT. In other words, we can use SAT to solve any problem in NP.
It turns out there are many problems in NP-complete. The fast conversion applies among them too, so in some sense, problems in NP-complete are all the same because we can use them all to solve instances of each other. However, for some of those problem instances the best known algorithm is to try all possible inputs, which requires exponential time (very, very slow for even modestly large inputs).
Lots of research has been and continues to be poured into SAT because any gains automatically yield improvements to everything else in NP-complete and the rest of NP. Using a SAT solver allows you to hitch a ride more or less for free on the results of all that research. Each incremental improvement to SAT solvers benefits programs that use them.
As the author noted, forming SAT instances by hand can be a pain. SMT or SAT Modulo Theories is sort of a high-level language that “compiles down” to SAT. Expressing problems with SMT is more natural and reduces the burden of converting your problem to SMT and SMT solutions back to your problem domain.
For toy-sized problems such as the LinkedIn Queens, 8-queens, and 9x9 Sudoku more or less any competently implemented solver will work fine. As soon as the size of the problem starts to grow, the difference between a plain backtracking algorithm and a SAT/SMT/CP system.
Next I want to try to solve the Tango and Zip games.
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?
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
> "Satisfiability Modulo Theories"
> Ryan solved this by writing Queens as a SAT problem, expressing properties like "there is exactly one queen in row 3" as a large number of boolean clauses. Go read his post, it's pretty cool. What leapt out to me was that he used CVC5, an SMT solver. (...) SMT solvers are "higher-level" than SAT, capable of handling more data types than just boolean variables. It's a lot easier to solve the problem at the SMT level than at the SAT level. To show this, I whipped up a short demo of solving the same problem in Z3 (via the Python API).