6 ms·

I wonder what is the target audience of articles like this. I think the article is well-written, however 90-95% of the terminology make little or no sense to me

I wonder what is the target audience of articles like this. I think the article is well-written, however 90-95% of the terminology make little or no sense to me who is not proficient in this field. Would the article be useful for someone who _is_ proficient in the field?

bjarneh 3y ago
> 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.
- sanxiyn 3y ago
  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.
  - c-cube 3y ago
    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.
  - bjarneh 3y ago
    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.
    - sanxiyn 3y ago
      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.
  - zero_k 3y ago
    That is true, but there are many interesting heuristics in modern SAT solvers, such as kissat: https://github.com/arminbiere/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 https://github.com/arminbiere/cadical I personally also develop a SAT solver called CryptoMiniSat, but the above two are easier to read :)
Jaxan 3y ago
The target audience is members of the acm. So that mostly includes computer science researchers, I guess.
YeGoblynQueenne 3y ago
It's not just you. I found the technical sections of the article impenetrable. And yet my background is on resolution theorem-proving (I did my PhD research on Inductive Logic Programming) and I read the article wishing to understand how CDCL is related to Resolution, but I couldn't figure that out. I don't have a background in SAT solving but the "clause learning" in CDCL looks a lot like what we call a Resolution-derivation in Resolution theorem-proving. In short, given a conjunction of two (propositional or first order) clauses (¬φ ∨ ψ) ∧ (φ ∨ χ) Resolution eliminates the contradiction in the "complementary pair" (¬φ, φ) and derives the new clause ψ ∨ χ. If that's what CDCL folk call learning then that's really interesting to me because most of Inductive Logic Programming is an effort to use Resolution for inductive inference i.e. machine learning, but in logic. I guess I should check the article's bibliography. They reference s a textbook that might be useful ("Handbook of Satisfiability". Though one of the authors is an author of the article so that may not bode well for the textbook).
- xavxav 3y ago
  Conflict explanation in CDCL is entirely based around resolution, the idea being to take a conflicting set of clauses and apply resolution a bunch of times to “simplify” the conflict into its most general form.
  - YeGoblynQueenne 3y ago
    If I understand correctly what "conflicting" means, that process can't possibly result in an empty clause, as in Resolution refutation proofs, correct? What would be the gold standard reference for CDCL? Something that would be taught at an undergraduate class, say? Edit: after reading a bit on the net it seems like clause learning in CDCL is basically Resolution-derivation by input Resolution. Cool beans.
- js8 3y ago
  The resolution is actually also what 2SAT algorithm is doing.
  - 3y ago

bjarneh 3y ago

> 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.

sanxiyn 3y ago
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.
- c-cube 3y ago
  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.
- bjarneh 3y ago
  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.
  - sanxiyn 3y ago
    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.
- zero_k 3y ago
  That is true, but there are many interesting heuristics in modern SAT solvers, such as kissat: https://github.com/arminbiere/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 https://github.com/arminbiere/cadical I personally also develop a SAT solver called CryptoMiniSat, but the above two are easier to read :)

Jaxan 3y ago

The target audience is members of the acm. So that mostly includes computer science researchers, I guess.

YeGoblynQueenne 3y ago

It's not just you. I found the technical sections of the article impenetrable. And yet my background is on resolution theorem-proving (I did my PhD research on Inductive Logic Programming) and I read the article wishing to understand how CDCL is related to Resolution, but I couldn't figure that out. I don't have a background in SAT solving but the "clause learning" in CDCL looks a lot like what we call a Resolution-derivation in Resolution theorem-proving. In short, given a conjunction of two (propositional or first order) clauses (¬φ ∨ ψ) ∧ (φ ∨ χ) Resolution eliminates the contradiction in the "complementary pair" (¬φ, φ) and derives the new clause ψ ∨ χ. If that's what CDCL folk call learning then that's really interesting to me because most of Inductive Logic Programming is an effort to use Resolution for inductive inference i.e. machine learning, but in logic. I guess I should check the article's bibliography. They reference s a textbook that might be useful ("Handbook of Satisfiability". Though one of the authors is an author of the article so that may not bode well for the textbook).

xavxav 3y ago
Conflict explanation in CDCL is entirely based around resolution, the idea being to take a conflicting set of clauses and apply resolution a bunch of times to “simplify” the conflict into its most general form.
- YeGoblynQueenne 3y ago
  If I understand correctly what "conflicting" means, that process can't possibly result in an empty clause, as in Resolution refutation proofs, correct? What would be the gold standard reference for CDCL? Something that would be taught at an undergraduate class, say? Edit: after reading a bit on the net it seems like clause learning in CDCL is basically Resolution-derivation by input Resolution. Cool beans.
js8 3y ago
The resolution is actually also what 2SAT algorithm is doing.
- 3y ago