4 ms·
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 solv
by 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 agois the first use of former/latter consistent with the second?
- dataflow 3y agoI think so? Which part of it sounds inconsistent?
- waldrews 3y agoShould 'formal methods courses' go with 'proving NP-completeness' and 'algo courses' go with 'using SAT solvers?'
- dataflow 3y agoNo. 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 agoAh, 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 agoIn 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.....