https://gist.github.com/enigma/98ea0392471fa70211251daa16ce8...
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).
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).
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/
Shameless plug: I wrote a (admittedly very deriative) introduction with some examples I thought at the time were cool.
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.
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.
Terrific little puzzle, highly recommend it!
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?
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
TheBozzCL•22h ago
Next I want to try to solve the Tango and Zip games.