6 ms·

> ... modern SAT solvers are fast, neat and criminally underused by the industry. Modern SAT solvers are fast, neat and criminally undertaught by the universit

> ... modern SAT solvers are fast, neat and criminally underused by the industry. Modern SAT solvers are fast, neat and criminally undertaught by the universities. Seriously, why isn't this taught at the undergraduate level in CS70 [1] discrete math type courses or CS170 [2] analysis of algorithms type courses? [1] https://www2.eecs.berkeley.edu/Courses/CS70/ https://www2.eecs.berkeley.edu/Courses/CS70/ [2] https://www2.eecs.berkeley.edu/Courses/CS170/ https://www2.eecs.berkeley.edu/Courses/CS170/

deleted 3y ago
[deleted]
tanx16 3y ago
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.
- deleted 3y ago
  [deleted]
- deleted 3y ago
  [deleted]
- tgamblin 3y ago
  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 3y ago
    > 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 3y ago
      Yep, from SAT. Edited. Guess I typed that too fast :)
- dataflow 3y ago
  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.
  - waldrews 3y ago
    is the first use of former/latter consistent with the second?
    - dataflow 3y ago
      I think so? Which part of it sounds inconsistent?
      - waldrews 3y ago
        Should 'formal methods courses' go with 'proving NP-completeness' and 'algo courses' go with 'using SAT solvers?'
        dataflow 3y ago
        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 3y ago
        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.
  - tanx16 3y ago
    In the particular project I was talking about (see https://inst.eecs.berkeley.edu/~cs170/sp20/assets/project/spec.pdf 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.pdf https://people.eecs.berkeley.edu/~vazirani/algorithms/chap8.....
lower 3y ago
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.
- layer8 3y ago
  What example use-cases did you use? Just curious.
  - lower 3y ago
    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.
- _0ffh 3y ago
  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.
PartiallyTyped 3y ago
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.
sam0x17 3y ago
We learned SAT solvers and got to implement one in one of our courses. Completely forget which one it was though.

deleted 3y ago

[deleted]

tanx16 3y ago

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.

deleted 3y ago
[deleted]
deleted 3y ago
[deleted]
tgamblin 3y ago
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 3y ago
  > 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 3y ago
    Yep, from SAT. Edited. Guess I typed that too fast :)
dataflow 3y ago
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.
- waldrews 3y ago
  is the first use of former/latter consistent with the second?
  - dataflow 3y ago
    I think so? Which part of it sounds inconsistent?
    - waldrews 3y ago
      Should 'formal methods courses' go with 'proving NP-completeness' and 'algo courses' go with 'using SAT solvers?'
      - dataflow 3y ago
        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 3y ago
        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.
- tanx16 3y ago
  In the particular project I was talking about (see https://inst.eecs.berkeley.edu/~cs170/sp20/assets/project/spec.pdf 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.pdf https://people.eecs.berkeley.edu/~vazirani/algorithms/chap8.....

lower 3y ago

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.

layer8 3y ago
What example use-cases did you use? Just curious.
- lower 3y ago
  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.
_0ffh 3y ago
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.

PartiallyTyped 3y ago

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.

sam0x17 3y ago

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