Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: