Understanding SAT by Implementing a Simple SAT Solver in Python (2014)

Correct me if I'm wrong, but this is usually not handled by SAT solvers, is it?

Internally we use SAT solvers to schedule resources on medical devices which makes the device look "smart", but this is not AI...

SAT is best when there is one true logical answer. ANN are best when you want "best advice".

A good guide (in my experience) -- with SAT while the answer is hard to find it's easy to check (like a Sudoku, or building a timetable with no clashes), while ANN give answers where verifying the answer isn't easy to perform computstionally (if I give you a translation of a text into Latin, verifying it is about as hard as just making a new one from scratch)

There are many ways to see differences between the two.

One is heuristic vs algorithm. If SAT solver finds a solution, it's correct. If ANN finds a solution, it might be correct.

ANN is suitable for pattern recognition, statistical learning and representation learning. Learning continuous functions for example. SAT solvers work best for discrete problems.

Deep neural networks don't help with problems where there is no solution; neural networks approximate functions where the explicit form of the function is unknown. For example nobody knows how to implement isCat(animal) without using machine learning, but we have enough data on cats to approximate said function without much trouble.

SAT solvers work out if it is possible to satisfy a logical model (hence the name).

In theory a neural network could approximate a function that solves SAT. In practice it is a much better idea to use a SAT solver. Neural networks aren't that powerful at solving logic puzzles.

I feel like I both agree and disagree. It is true that beating glucose or lingeling at the SAT competition would require a lot more engineering than just plain CDCL + 2 literal watching. At the same time, I think a lot of the new stuff (which in my book is everything that's happened in SAT post 2007ish) is primarily focused on winning the SAT competition by taking a sort of kitchen-sink approach.

For instance, CryptoMinisat first implemented XOR detection along with Gaussian elimination. They were using SAT on cryptographic problems, so it made sense to specialize for that domain. But now there's a bunch of crypto-based problems in the SAT competition and many of the other solvers also implement Gaussian elimination. But I'd guess that most users of SAT solvers wouldn't see a noticeable performance difference if you got rid of Gaussian elimination from the solvers.

Another good example is Alan Mischenko's ABC which wins the hardware model checking competition every year but uses a fairly ancient version of MiniSAT as its SAT solving engine. It's not that a faster solver wouldn't make ABC faster, but that the real smarts in model checking are in what queries you send to the solver, not in squeezing an extra 2X or 3X performance out of the SAT solver using the same old dumb queries.