[R] I need a name - Page 3

On April 28 2008 23:57 berated- wrote:


That's really kind of irrelevant to the project. I'm taking a boolean satisfiability class and we have to do a final project related to boolean equations. Considering I'm not a total badass, I knew I wasn't going to come up with the next great thing such as WalkSAT or Davis Putnam or GSAT, any of the SAT solving techniques that were monumental upon release. So I was left with two options, I could either find some current research and write an 8 page paper on it, or I could code up an algorithm.

Reading conference papers didn't strike me as overly fun, so I went with a coding project. I could then do something like just pass a boolean equation to an algorithm and try to solve it, which would have got the job done but is a little bland. So I sought out something that would at least be enjoyable.

As for the original question, my first response would have to be no. Using DP, a true sudoku puzzle ( one with only one answer and requiring no search techniques ) would actually require only unit propagation while solving the algorithm. Of course, you would have to define what it is inefficient compared to. Its obviously better than a try all possibilities solution. Are there other algorithms out there that might do better? I have no idea. I wasnt studying Sudoku, I was studying boolean equations, so I apologize that I can't give you a better answer.

I guess you would have to make that judgment call:

My technique ( learned from the work of others who have already done this - I'm just an undergrad, I can't be doing monumental work in my field ):

There are 729 variables - one for every possible number in every possible cell. These are represented by a 3 digit string - the row, the column, and the number.

So 111 refers to a one being in the upper left most box, and will be a 1 if there is a 1 there, 0 otherwise. A - in front represents that the boolean is negated. so -111 refers to Not a 1 in the upper left hand box

Then you have to generate the equation, it will be in CNF form -

So the first thing to check is that there is a 1-9 in every cell.
so, 111 v 112 v 113 v 114 v 115 v 116 v 117 v 118 v 119
but then you need to make sure there aren't more than one
so
-111 v -112, -111 v -113 . . . etc

Repeat for rows, columns, and boxes.

And solve.

Edit: Okay, well yes I would say that having a SAT solver for a 9x9 sudoku puzzle is a little over the top. I knew that it was for a 9x9, but I guess I didn't realy realize how much over the top it was. Of course, it doesn't help that I'm using a lot of java classes - trying to really modularize my code to make it easier to understand and write.

Using strictly ints and try all possibilities it takes java about 64 ms to solve a sudoku puzzle. Using my sat solver it takes about 400ms to solve - however, the largest time with my solver is keeping track of which variables I flipped and which ones I didn't, because I have to store and reset the variables while backtracking.

It might be kind of interesting to mod my program and then try to see some results. I've seen some sat solvers that use strictly ints ( as i described the 111 stuff above, all that is ints while i use 4 different wrapper classes to keep the method writing short). I think that if I were go get my program working in that state, and then we compared the run times you would see a lot closer of a contest.

Where I think the SAT solver would really shine would be on the larger puzzles for a generalized sudoku puzzle of size nxn. I would guess that even at 16x16 the sat solver ( if done properly with int values instead of classes ) would already start to out due the try all possibilities approach.

Once again though, I had fun with the project and truly believe it will still get me an A, so I'm not too worried about the efficiency. Hope this explain things a little better, and thanks for the thought provoking question.

On April 29 2008 07:22 azndsh wrote:


yeah... with 729 variables and thousands of restrictions, it seems like it would take a very long amount of time for non-trivial puzzles. I only ask because we were each asked to make a SAT solver and puzzle generator in one of my CS classes. We even had a competition to see who had the best solver in the end. One really simple and effective heuristic is to assume that all your variables are false at the beginning, which in this case is true 8/9 of the time.

I ended up doing a 4x4 version of sudoku puzzles, but that was relatively straightforward and ran very quickly.