Indeed! Here is Sudoku, formulated as a SAT problem. You can use for example SICStus Prolog to run it:

    sudoku(Rows) :-
            length(Rows, 9), maplist(same_length(Rows), Rows),
            maplist(row_booleans, Rows, BRows),
            maplist(booleans_distinct, BRows),
            transpose(BRows, BColumns),
            maplist(booleans_distinct, BColumns),
            BRows = [As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is],
            blocks(As, Bs, Cs), blocks(Ds, Es, Fs), blocks(Gs, Hs, Is).

    blocks([], [], []).
    blocks([N1,N2,N3|Ns1], [N4,N5,N6|Ns2], [N7,N8,N9|Ns3]) :-
            booleans_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]),
            blocks(Ns1, Ns2, Ns3).

    booleans_distinct(Bs) :-
            transpose(Bs, Ts),
            maplist(card1, Ts).

    card1(Bs) :- sat(card([1],Bs)).

    row_booleans(Row, Bs) :-
            same_length(Row, Bs),
            maplist(cell_boolean, Row, Bs).

    cell_boolean(Num, Bs) :-
            length(Bs, 9),
            sat(card([1],Bs)),
            element(Num, Bs, 1).

This uses the sat/1 constraint to denote Boolean satisfiability.

Here is an example Soduku problem, taken from Donald Knuth's The Art of Computer Programming:

    knuth(b, [[1,_,3,_,5,6,_,8,9],
              [5,9,7,3,8,_,6,1,_],
              [6,8,_,1,_,9,3,_,5],
              [9,5,6,_,3,1,8,_,7],
              [_,3,1,5,_,8,9,6,_],
              [2,_,8,9,6,_,1,5,3],
              [8,_,9,6,_,5,_,3,1],
              [_,6,5,_,1,3,2,9,8],
              [3,1,_,8,9,_,5,_,6]]).

Sample query and result:

    ?- knuth(b, Rows),
       sudoku(Rows),
       maplist(portray_clause, Rows).
    [1, 2, 3, 4, 5, 6, 7, 8, 9].
    [5, 9, 7, 3, 8, 2, 6, 1, 4].
    [6, 8, 4, 1, 7, 9, 3, 2, 5].
    [9, 5, 6, 2, 3, 1, 8, 4, 7].
    [7, 3, 1, 5, 4, 8, 9, 6, 2].
    [2, 4, 8, 9, 6, 7, 1, 5, 3].
    [8, 7, 9, 6, 2, 5, 4, 3, 1].
    [4, 6, 5, 7, 1, 3, 2, 9, 8].
    [3, 1, 2, 8, 9, 4, 5, 7, 6].

SAT - Satisfiability

https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

Acronyms are always a pet peeve of mine. I would know what a SAT is - since I've spent more than 50% of my life with Computer Science. However, not many people would understand the acronym you'd use. So, it would be great if in general one mentions what SAT refers to rather than using the acronym. Mention the long form the first time and then use the short form later in your sentence.

Sorry if this came across as too affront, just a personal observation. I saw this a couple of ago with GRUs on another thread too.

I think "SAT solver" gives a sufficient hint?

yes, a NN isn't the best tool for the job. i guess it's just an experiment if one was able to do this with a reasonable rate of success.

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.

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.

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.

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.

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.

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!

I just want to mention that this NN code is as simple as it gets and that anyone remotely knowing what they're doing could code op's thing in about 2 hrs.

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.

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

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.

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.

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.

None of the alternatives I proposed require domain knowledge, they just require you to state the sudoku rules, which is inevitable.

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.

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.

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

Even a SAT solver is overkill.