4 ms·

There are no easy way to solve SAT as the size of sudoku. Modern day SAT solvers are very large and contains years of experience, containing 10s of heuristics a

There are no easy way to solve SAT as the size of sudoku. Modern day SAT solvers are very large and contains years of experience, containing 10s of heuristics and complex structures. If we can simplify using neural network, I think it's a great step.

brian_herman 9y ago
We did use a library for the SAT solving. Hmm didn't think of that though.
jakob223 9y ago
I don't know that neural netowrks are particularly "simpler" than SAT solvers. They're both complex general tools with different requirements of problem knowledge.
taeric 9y ago
I'd be surprised if NNs come up with a simpler result. At least, not one that has anything close to intuitive results. That is, yes, sat solvers have a lot of heuristics to speed them up. But, almost by definition, we understand those heuristics do can reason about the answers they give. NNs, however, are notorious for being incredibly opaque. They give his probabilistic answers, but my understanding is we really only trust them probabilistically and can't explain their answers.
contravariant 9y ago
Well, it is really more of a exact cover problem, which can be solved quite simply and elegantly with Knuth's algorithm X. A neural network isn't simpler in any sense of the word. You might as well throw a simulated annealer at the problem.
- deleted 9y ago
  [deleted]
- likelynew 9y ago
  I am not saying it is not. My condition is in what if neural network can solve a problem without any domain knowledge. I think it's a huge win even if we don't understand anything about the solution. Be it well solved problems like approximate minimum distance in a graph to practically unsolvable like automatically proving unproved theorems in mathematics.
  - contravariant 9y ago
    None of the alternatives I proposed require domain knowledge, they just require you to state the sudoku rules, which is inevitable.
  - likelynew 9y ago
    I take it this way. How many problems can you solve using knowing mostly exact cover. Not very many. But, if we can build ML systems that can solve mostly any problem(we can't today) even without giving any insight, I would say it will be one of the things whose impact will surpass anything. Note, I am not getting into AGI, just saying a system that can solve objective problems. And while sudoku is not a very good example, but I think it shows we can do many cool things from neural networks. Neural networks are the most sure bet for such a system.
    - taeric 9y ago
      You'd be surprised how far exact cover can get you. The trick isn't in knowing exact cover, per se. But in seeing how to map problems to different problems. That is, the "exact cover" nature of Sudoku is not immediately obvious to everyone. At least, it wasn't obvious to me. Seeing how quickly you can map it to that and then get a solution was a lot of fun and ridiculously educational.
- microtherion 9y ago
  > A neural network isn't simpler in any sense of the word. You might as well throw a simulated annealer at the problem. Great idea! I'm sure D-WAVE would be happy to work with you on a quantum sudoku solver.
CJefferson 9y ago
Reasonably modern SAT solvers (Say MiniSAT) have a lot less complexity than a modern neural network. Also, I set as a intro to C practical writing a SAT solver which can easily solve any real-world Sudoku instance.
- likelynew 9y ago
  Are you serious.. SAT solvers have some of the hardest code I have seen. Look at the SAT solvers that won satcompetition. On the other hand IMO, implementing a neural network on your own is very easy. But the point is not that. I consider the neural network libraries(e.g. tensorflow) as given, as it is in not related to the problem, and can be used in many different problems. I will consider only the code above the neural network API for the complexity(like models, encoding etc.). But a SAT solver has a specific function and is core part of the problems it is trying to solve.
  - CJefferson 9y ago
    There are super-complicated SAT solvers certainly, but MiniSAT has (in my opinion) reasonably easy to understand code. It's not very long either. Have you tried reading the code to Tensorflow? Also, in my personal experience, SAT is currently applicable to more problems than Neural Networks (although that is changing as Neural Networks get applied to more things). You can use SAT solvers to solve any problem in NP (well, other things as well but it rapidly gets painful). That's a lot of problems!
  - taeric 9y ago
    I think you are running afoul of not realizing that "world class" neural networks are a ton of code. Just as a trivial SAT solver is easy and can be implemented rather quickly. Now, neither will be that good at the job they are made for. But that is far from unique to this field. Consider, a car/bike/house/whatever is not exactly hard to build for backyard use. Getting world class, on the other hand, escalates to difficult very quickly.
  - joshuata 9y ago
    Yes, competitive SAT solvers are very complicated. However, they are not outside of most developers' abilities. During a verification course at my University we had to build a simple SAT solver. Most students were able to complete the project in ~20-30 hours. Mine wasn't fast, but it worked well enough to be a proof of concept. Also, saying that NN are easy with a library like tensorflow is akin to saying that Sudoku solvers are easy with Prolog. Of course they are! The library/language does the vast majority of the heavy lifting.

brian_herman 9y ago

We did use a library for the SAT solving. Hmm didn't think of that though.

jakob223 9y ago

I don't know that neural netowrks are particularly "simpler" than SAT solvers. They're both complex general tools with different requirements of problem knowledge.

taeric 9y ago

I'd be surprised if NNs come up with a simpler result. At least, not one that has anything close to intuitive results. That is, yes, sat solvers have a lot of heuristics to speed them up. But, almost by definition, we understand those heuristics do can reason about the answers they give. NNs, however, are notorious for being incredibly opaque. They give his probabilistic answers, but my understanding is we really only trust them probabilistically and can't explain their answers.

contravariant 9y ago

Well, it is really more of a exact cover problem, which can be solved quite simply and elegantly with Knuth's algorithm X. A neural network isn't simpler in any sense of the word. You might as well throw a simulated annealer at the problem.

deleted 9y ago
[deleted]
likelynew 9y ago
I am not saying it is not. My condition is in what if neural network can solve a problem without any domain knowledge. I think it's a huge win even if we don't understand anything about the solution. Be it well solved problems like approximate minimum distance in a graph to practically unsolvable like automatically proving unproved theorems in mathematics.
- contravariant 9y ago
  None of the alternatives I proposed require domain knowledge, they just require you to state the sudoku rules, which is inevitable.
- likelynew 9y ago
  I take it this way. How many problems can you solve using knowing mostly exact cover. Not very many. But, if we can build ML systems that can solve mostly any problem(we can't today) even without giving any insight, I would say it will be one of the things whose impact will surpass anything. Note, I am not getting into AGI, just saying a system that can solve objective problems. And while sudoku is not a very good example, but I think it shows we can do many cool things from neural networks. Neural networks are the most sure bet for such a system.
  - taeric 9y ago
    You'd be surprised how far exact cover can get you. The trick isn't in knowing exact cover, per se. But in seeing how to map problems to different problems. That is, the "exact cover" nature of Sudoku is not immediately obvious to everyone. At least, it wasn't obvious to me. Seeing how quickly you can map it to that and then get a solution was a lot of fun and ridiculously educational.
microtherion 9y ago
> A neural network isn't simpler in any sense of the word. You might as well throw a simulated annealer at the problem. Great idea! I'm sure D-WAVE would be happy to work with you on a quantum sudoku solver.

CJefferson 9y ago

Reasonably modern SAT solvers (Say MiniSAT) have a lot less complexity than a modern neural network. Also, I set as a intro to C practical writing a SAT solver which can easily solve any real-world Sudoku instance.

likelynew 9y ago
Are you serious.. SAT solvers have some of the hardest code I have seen. Look at the SAT solvers that won satcompetition. On the other hand IMO, implementing a neural network on your own is very easy. But the point is not that. I consider the neural network libraries(e.g. tensorflow) as given, as it is in not related to the problem, and can be used in many different problems. I will consider only the code above the neural network API for the complexity(like models, encoding etc.). But a SAT solver has a specific function and is core part of the problems it is trying to solve.
- CJefferson 9y ago
  There are super-complicated SAT solvers certainly, but MiniSAT has (in my opinion) reasonably easy to understand code. It's not very long either. Have you tried reading the code to Tensorflow? Also, in my personal experience, SAT is currently applicable to more problems than Neural Networks (although that is changing as Neural Networks get applied to more things). You can use SAT solvers to solve any problem in NP (well, other things as well but it rapidly gets painful). That's a lot of problems!
- taeric 9y ago
  I think you are running afoul of not realizing that "world class" neural networks are a ton of code. Just as a trivial SAT solver is easy and can be implemented rather quickly. Now, neither will be that good at the job they are made for. But that is far from unique to this field. Consider, a car/bike/house/whatever is not exactly hard to build for backyard use. Getting world class, on the other hand, escalates to difficult very quickly.
- joshuata 9y ago
  Yes, competitive SAT solvers are very complicated. However, they are not outside of most developers' abilities. During a verification course at my University we had to build a simple SAT solver. Most students were able to complete the project in ~20-30 hours. Mine wasn't fast, but it worked well enough to be a proof of concept. Also, saying that NN are easy with a library like tensorflow is akin to saying that Sudoku solvers are easy with Prolog. Of course they are! The library/language does the vast majority of the heavy lifting.