Martin Hořeňovský, a C++ developer, writes about SAT solvers, C++ random numbers, CMake, and testing.
Commenters point to his SAT solver series as a clear overview of why generic solvers are underused, and to his CMake guide.
A closely related technique to SAT solvers is the "Constraint Satisfaction Problem" which I've been looking into recently.
Constraint Programming and SAT are BOTH NP-complete problems, and as such, they are mathematically equivalent. However, its sometimes more "obvious" to write problems in one form vs the other.
For example, Sudoku is simply written 27 constraints:
* All Different (X11, X12, X13, X14, X15, X16, X17, X18, X19)
* All Different (X21, X22, X23, X24, X25, X26, X27, X28, X29)
...
* All Different (X11, X21, X31, X41, X51, X61, X71, X81, X91)
...
* All Different (X11, X12, X13, X21, X22, X23, X31, X32, X34)
...
etc. etc.
Then define each "X" variable as "between 1 and 9" and bam, you're done with defining the problem in terms of "Constraints".
Representing Sudoku as a SAT problem is possible of course, but its just... harder. It just feels more humanly natural to represent Sudoku in terms of constraints. Or maybe not. Read "Part 1" if you want to see how the original blogger solved it in terms of 3-SAT (https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/)
----------
Here's an article from IBM hyping up their "CPLEX" Constraint solver for Sudoku for example: https://www.ibm.com/developerworks/community/blogs/jfp/entry/solving_the_hardest_sudoku?lang=en
----------
Anyway, just plugging in a similarly fast, neat, and underused (and mathematically equivalent) solver to what the blogpost talks about. I personally don't know too…
That's not really an option for me when I debug C++ that is run on a Linux or Android TV. It also wouldn't be an option when I used to work with C++ that was used on Linux servers. That's a big chunk of C++ use.
While I have your attention, I see your comments here in C++ threads quite often. You seem to like the language and at the same time you have some experience with simpler languages like Oberon. My experience with C++ has been that people happily go on to create giant inheritance hierarchies, with no restraint for multiple inheritance to the point that it's so unmanagable that nobody knows where things go and what actually happens. With all that inheritance, they lose track that the same thing has actually been copied tens of times between different classes and now these tens of classes have code that is basically copy-pasted and who knows what benefit anyone has from all this inheritance. Google engineers are one of the offenders when it comes to overuse of inheritance. Then, modern C++ allegedly fixes some warts, but IME it introduces more of them. E.g. the initialization fiasco (I honestly can't say with 100% confidence what braces do when you initialize std::vector). Then there is this thing that when you create a lambda like so:
[&] { ... }
And then move it to a function which will create lambdas of this form, just with different captures:
std::function<void()> create_lambda(args...) {
return [&] { ... };
}
The second version will crash later…
The article series Modern SAT Solvers: Fast, Neat, and Underused[1] argues that we don't use generic problem solvers enough in our daily engineering work.
A generic solution won't beat a hand-optimised specific solution, but if you're good at phrasing your problem in the right way, you can get 80 % of the way there with 20 % of the effort by using a generic solver.
Z3, being an even more generic SMT solver rather than "just" a SAT solver, should allow you to do even more with less.
I've long wanted to integrate this type of solver into my workflow more, because I think that if I can make it into more of a habit, it would provide insane leverage for prototyping. Does anyone have experience using these techniques for that?
[1]: https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/
I'm not familiar with that game, but depending on what the goal is, I think you have three options:
- if you want to check that a complex system of rules has a solution, then you can translate that into a SAT problem and run a SAT solver (https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/)
- if the problem is small enough, you could run an exhaustive search of options - in that case it really doesn't matter how you encode the rules, it could be any function returning a bool
- if you're trying to prove some invariant about the game, look at languages like Coq - they should help you
I'm surprised not to see any mention of satisfiability here. There are a few papers I've seen about it, but this blog post seems to give a reasonable overview:
https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/
Then you just need to start counting models, which is the #SAT (sharp SAT) problem:
https://en.wikipedia.org/wiki/Sharp-SAT
Using software such as:
https://github.com/marcthurley/sharpSAT
The author does discuss this in a footnote:
https://codingnest.com/basic-cmake/#fn4
In this case, I think I agree. Otherwise ya, try to avoid set. Except for CACHE variables, I think.