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.

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.

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

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

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.

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

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

I think so? Which part of it sounds inconsistent?

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

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.

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.

I used to teach formal methods at university, including a course with a lot of SAT examples. We tried to make it as practical as possible, with many examples and exercises in Java (where you just generate your formulas and call a solve method). Thing is, most students seemed to hate it passionately, just like with reductions to SAT in complexity theory.

I wrote a bespoke backtracking solver for a specific class of problems. Would love to use Z3 or something, but frankly, I wouldn't know how to systematically translate problem instances to solver constraints. It's essentially a kind of very complex job-shop scheduling problem with lots of dynamic inter-dependencies. Many of the problems are hard to even solve without dead-locking, while we also naturally strive to minimize overall processing time. Where would I find ressources to help me get a grip on my specific problem [1]? Could I reasonably hope that Z3 or another general solver might be faster than a moderately well designed bespoke solver in a compiled language? (My solver combines a bunch of greedy heuristics with a backtracker in case it runs into a dead-lock, which is often.)

[1] Rough problem outline: Input goods must be transformed through a complex series of assembly/machining/processing lines to output goods; each line transforms one or two inputs into an (intermediary or end-) product; an assembly line produces it's product in a fixed number of time units and cannot be stopped or delayed; finished intermediary products arrive at the end of an assembly line, which must be cleared by then; there are a limited number of temporary storage spaces where intermediary products can be moved to/from in a fixed number of time units; some assembly lines must wait for two intermediary products to be completed to start a job combining them into another intermediary or end product; end products must then be moved to their destinations.

The pdf linked on this site is the biggest collection of SMT examples I know of: https://sat-smt.codes/

I’m no SMT expert, but the way I’ve done it is to make some representation in Python Z3, and then write some function or class that generates those. I was solving MLB eliminations (more complex than it sounds) and I think I used arrays of ints for number of wins. So I’d pull MLB data, turn that into schedule objects which turned themselves into z3 constraints.

This type of problem is more the domain of Constraint Programming (a related field). Job-scheduling problems are pretty much the main focus. I would look up MiniZinc (it even comes with a nice IDE) and see if you can grok it.

What example use-cases did you use? Just curious.

We've had various examples like these:

- Puzzles: Sudoku, St8ts

- Bridge crossing: Missionaries and cannibals, 17 minute bridge crossing (I need a computer to solve this anyway)

- Concurrency: finding bug in mutual exclusion algorithm (Peterson algorithm with a bug)

- Graphs: coloring a map, finding a Hamilton path

- Sorting: Finding bugs in a sorting network

For many students it was difficult to encode problems in SAT. They seemed to understand given example encodings, but then found it difficult to vary them. There is a lot of freedom in how one may encode things and it's hard at first to debug at first when things don't work in the way you're expecting. If there is no solution, then one needs to investigate where there are unwanted constraints or errors in the encoding. If there are unwanted solutions, one needs to identify the missing constraints. It was hard to get across how to do this and it's probably frustrating for beginners.

Both my Alma Maters had courses that used these extensively, and also planners like (Pl|Tr|L)ingeling. We also covered reducability and SAT in multiple courses in both.

These should also be taught in an advanced PL course, e.g liquid, dependent etc types.

We learned SAT solvers and got to implement one in one of our courses. Completely forget which one it was though.