[tanx16]

This is… not true. CS170 specifically teaches about reducing NP problems to SAT (you can find this in the Algorithms textbook linked in the class syllabus). I recall solving one of the projects by using MiniSat after converting a problem to 3-SAT. FWIW, the textbook is excellent and the course was very useful.

[tgamblin]

I definitely recall doing reductions from SAT in Algorithms courses. I think that is a common part of most curricula.

I don't recall being taught any practical uses of SAT. It was introduced only in the context of Cook's theorem, as the problem you needed to reduce to other problems in order to show NP-completeness.

I think most people now learn SAT in that theoretical context, not as a tool to solve problems.

[dataflow]

> I definitely recall doing reductions to SAT in Algorithms courses.

> It was introduced only in the context of Cook's theorem, as the problem you needed to reduce other problems to in order to show NP-completeness.

Are you referring to reductions from SAT, or to SAT? You seem to be mentioning both?

[tgamblin]

Yep, from SAT. Edited. Guess I typed that too fast :)

[dataflow]

To clarify, you're specifically talking about reductions to SAT, not from SAT, right?

Note the former is used as a solution technique for feeding into SAT solvers, where the latter's goal is basically the exact opposite (to show NP-hardness and hence algorithmic intractability). Formal methods courses do the former, but algorithms courses usually use SAT for the latter.

[tanx16]

In the particular project I was talking about (see https://inst.eecs.berkeley.edu/~cs170/sp20/assets/project/sp... for a similar project) a solution is to reduce the problem to SAT and feed it into a SAT solver. Outside of the project, we were also taught the other way around (demonstrate NP-hardness). See https://people.eecs.berkeley.edu/~vazirani/algorithms/chap8.....

[waldrews]

is the first use of former/latter consistent with the second?

[dataflow]

I think so? Which part of it sounds inconsistent?

[waldrews]

Should 'formal methods courses' go with 'proving NP-completeness' and 'algo courses' go with 'using SAT solvers?'

[dataflow]

No. Algorithms courses focus on computability and complexity (including NP-completeness); they don't generally focus on SAT solving. Formal methods are the ones that use SAT solving, SMT solving, etc. to formally prove correctness.

[waldrews]

Ah, thank you. We had theory classes with automata and reductions and complexity proofs, and then algorithms classes that covered some solving techniques. I think I mixed up Formal Methods with Theory.