> Would the article be useful for someone who _is_ proficient in the field?
Yes, it is a very well written summary of what has been going on with SAT solvers in the last decades. I personally think most of this (r)evolution can be attributed to miniSAT. A relatively easy to read (at least compared to other theorem provers), free software implementation of a SAT solver, with instantiations if I remember correctly. Since variables only have two possible valuations (true/false) in boolean logic, they can be instantiated and the problem can be split up, and sometimes greatly simplified in doing so. I.e. we can replace each occurrence of variable 'a' with 'true' to make a new smaller problem, and then replace each occurrence variable 'a' with 'false' to make another smaller problem. I.e. split 1 problem into 2 simpler problems, and solve them in parallel etc.
As I remember, Glucose was a larger advance than MiniSat. MiniSat was well-engineered but not exceptional. Glucose started as a hack, but the heuristic it introduced was so effective that you basically couldn't compete without copying it.
That is true, but there are many interesting heuristics in modern SAT solvers, such as kissat: https://github.com/arminbiere/kissat (winner for a few years now). LBD ("glues" in glucose) is one of them. Kissat is actually quite readable. More readable is CaDiCaL, also extremely fast and effective: https://github.com/arminbiere/cadical
I personally also develop a SAT solver called CryptoMiniSat, but the above two are easier to read :)
Glucose was a patch on minisat I think. So it couldn't have existed without minisat and its exceptional popularity. For a while there was even a category at the competition where entrants had to be small modifications of minisat.
You could be correct. I haven't worked in academia for about 12 years; and I mostly worked on other types of logic. I do remember miniSAT being praised for its openness and readability, and it seems to predate the Glucose solver by some years. I.e. "in my day" miniSAT had all the praise, but perhaps Glucose was a more important contribution to the field.
FWIW, Knuth's chapter on satisfiability mentions MiniSat once for historical interest and discusses Glucose heuristic for five pages. This matches my impression of their technical contributions.
Yes, it is a very well written summary of what has been going on with SAT solvers in the last decades. I personally think most of this (r)evolution can be attributed to miniSAT. A relatively easy to read (at least compared to other theorem provers), free software implementation of a SAT solver, with instantiations if I remember correctly. Since variables only have two possible valuations (true/false) in boolean logic, they can be instantiated and the problem can be split up, and sometimes greatly simplified in doing so. I.e. we can replace each occurrence of variable 'a' with 'true' to make a new smaller problem, and then replace each occurrence variable 'a' with 'false' to make another smaller problem. I.e. split 1 problem into 2 simpler problems, and solve them in parallel etc.