Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.python > #87940 > unrolled thread

Sudoku solver

Back to article view | Back to comp.lang.python

Contents

  Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-25 13:39 +0200
    Re: Sudoku solver John Ladasky <john_ladasky@sbcglobal.net> - 2015-03-25 11:44 -0700
      Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-25 13:05 -0600
      Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-25 21:37 +0200
        Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-25 14:09 -0600
          Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-25 22:31 +0200
            Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-26 09:40 +1100
            Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-25 18:07 -0600
              Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-27 20:04 +0000
            Re: Sudoku solver Abhiram R <abhi.darkness@gmail.com> - 2015-03-26 08:26 +0530
            Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-25 21:24 -0600
            Re: Sudoku solver Abhiram R <abhi.darkness@gmail.com> - 2015-03-26 08:58 +0530
              Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 14:13 +0200
                Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 16:15 +0200
            Re: Sudoku solver albert@spenarnc.xs4all.nl (Albert van der Horst) - 2015-04-10 23:10 +0000
        Re: Sudoku solver Sayth <flebber.crue@gmail.com> - 2015-03-27 20:39 -0700
          Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-28 23:50 +0000
            Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-29 11:12 +1100
              Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 21:59 +0100
                Re: Sudoku solver Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-03-29 22:19 +0100
                  Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 22:59 +0100
            Re: Sudoku solver Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-03-29 14:06 +1100
              Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-29 15:10 +1100
                Re: Sudoku solver Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-03-29 21:35 +1100
                  Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-29 21:54 +1100
                  Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 13:01 +0100
                    Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 16:23 +0100
              Re: Sudoku solver Christian Gollwitzer <auriocus@gmx.de> - 2015-03-29 09:57 +0200
                Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-30 11:54 +0100
              Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 12:25 +0100
                Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-29 21:03 +0300
                  Re: Sudoku solver Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-03-29 19:26 +0100
                    Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-29 21:33 +0300
                  Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 22:11 +0100
                  Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-30 00:50 -0600
                    Re: Sudoku solver Christian Gollwitzer <auriocus@gmx.de> - 2015-03-30 09:13 +0200
                      Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-30 01:29 -0600
                        Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-30 12:16 +0300
                      Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-30 04:16 -0400
                      Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-30 02:57 -0600
                      Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-30 20:13 +1100
            Re: Sudoku solver Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-03-29 22:21 +0100
              Re: Sudoku solver BartC <bc@freeuk.com> - 2015-03-29 23:17 +0100
                Re: Sudoku solver Seymore4Head <Seymore4Head@Hotmail.invalid> - 2015-03-29 21:40 -0400
    Re: Sudoku solver Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-03-26 09:50 +1100
      Re: Sudoku solver Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-03-25 23:04 +0000
        Re: Sudoku solver Christian Gollwitzer <auriocus@gmx.de> - 2015-03-27 07:40 +0100
    Re: Sudoku solver "Frank Millman" <frank@chagford.com> - 2015-03-26 10:19 +0200
      Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 14:26 +0200
        Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-26 23:37 +1100
        Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-26 07:15 -0600
          Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 16:23 +0200
            Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-26 09:06 -0600
              Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 17:48 +0200
                Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-26 10:20 -0600
                  Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 18:47 +0200
        Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-26 10:14 -0400
        Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-27 01:41 +1100
        Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-26 11:03 -0400
          Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-26 17:42 +0200
            Re: Sudoku solver Pete Forman <petef4+usenet@gmail.com> - 2015-03-26 22:24 +0000
        Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-27 02:21 +1100
        Re: Sudoku solver Dennis Lee Bieber <wlfraed@ix.netcom.com> - 2015-03-26 20:42 -0400
        Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-27 09:14 -0400
        Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-28 00:25 +1100
        Re: Sudoku solver "Frank Millman" <frank@chagford.com> - 2015-03-27 15:35 +0200
          Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-27 15:56 +0200
            Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-27 10:09 -0400
              Re: Sudoku solver sohcahtoa82@gmail.com - 2015-03-27 11:18 -0700
                Re: Sudoku solver Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-03-28 12:46 +1100
              Re: Sudoku solver Larry Hudson <orgnut@yahoo.com> - 2015-03-27 16:48 -0700
            Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-28 01:07 +1100
            Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-28 01:19 +1100
              Re: Sudoku solver Gregory Ewing <greg.ewing@canterbury.ac.nz> - 2015-03-28 14:13 +1300
              Re: Sudoku solver Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2015-03-28 12:40 +1100
                Re: Sudoku solver Ian Kelly <ian.g.kelly@gmail.com> - 2015-03-28 02:24 -0600
            Re: Sudoku solver Mark Lawrence <breamoreboy@yahoo.co.uk> - 2015-03-27 16:03 +0000
            Re: Sudoku solver Virgil Stokes <vs@it.uu.se> - 2015-03-28 19:36 +0100
        Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-27 09:48 -0400
        Re: Sudoku solver Dave Angel <davea@davea.name> - 2015-03-27 09:52 -0400
        Re: Sudoku solver Chris Angelico <rosuav@gmail.com> - 2015-03-28 00:58 +1100
    Re: Sudoku solver mr.smittye@gmail.com - 2015-03-29 16:39 -0700
      Re: Sudoku solver Marko Rauhamaa <marko@pacujo.net> - 2015-03-30 12:24 +0300

Page 3 of 5 — ← Prev page 1 2 [3] 4 5  Next page →

#88328

On Mon, Mar 30, 2015 at 7:57 PM, Ian Kelly <ian.g.kelly@gmail.com> wrote:
> On Mon, Mar 30, 2015 at 2:16 AM, Dave Angel <davea@davea.name> wrote:
>> The relationship between row, column and box can be rearranged.  Some of
>> these are already covered by the rotations proposed earlier, where for a 90
>> degree rotate, row becomes column and column becomes row.  But in a similar
>> way each box could become a column, and so on.
>
> I don't think this one is valid. The intersection of a row and a
> column is one cell. The intersection of a row and a box is three
> cells. If you swap a column with a box, you're changing the
> relationships between the squares and the result will not be
> isomorphic to the original.

But if you swap *every* column with *every* box?

ChrisA

[toc] | [prev] | [next] | [standalone]

#88284

On 28/03/2015 23:50, BartC wrote:
> On 28/03/2015 03:39, Sayth wrote:
>> Good test for pypy to see where it's speed sits between C and Python.
>
> I've spent the last hour or so doing such tests.
>
> Using the OP's algorithm, and testing with the 'hard' puzzle posted by
> Ian Kelly, I got these approximate results:
>
> Python 3.1:     1700 seconds     (normal Python interpreter)
> PyPy:           93 seconds
> C unoptimised:  17 seconds       (gcc -O0 32-bit)
> C optimised:    3.3 seconds      (gcc -O3 32-bit)
> (X:             170 seconds)
>
> All running on Windows on x64.
>
> (X is my own interpreted language, which is where my interest in this
> is. This had been generally faster than Python until PyPy came along. It
> does however use a pure byte-code interpreter, so the result is not too
> bad.
>
> But using X *and* my own brute-force algorithm, the same puzzle took 2
> seconds to solve - faster than C!
>
> However it doesn't matter that the OP's algorithm is not great, as it
> makes an interesting new benchmark.)
>

https://attractivechaos.wordpress.com/2011/06/19/an-incomplete-review-of-sudoku-solver-implementations/

-- 
My fellow Pythonistas, ask not what our language can do for you, ask
what you can do for our language.

Mark Lawrence

[toc] | [prev] | [next] | [standalone]

#88289

On 29/03/2015 22:21, Mark Lawrence wrote:
> On 28/03/2015 23:50, BartC wrote:
>> On 28/03/2015 03:39, Sayth wrote:
>>> Good test for pypy to see where it's speed sits between C and Python.

>> Python 3.1:     1700 seconds     (normal Python interpreter)
>> PyPy:           93 seconds
>> C unoptimised:  17 seconds       (gcc -O0 32-bit)
>> C optimised:    3.3 seconds      (gcc -O3 32-bit)

> https://attractivechaos.wordpress.com/2011/06/19/an-incomplete-review-of-sudoku-solver-implementations/

"The fastest Sudoku solver can solve even the hardest Sudoku in about 1 
millisecond and solve most others in 0.1 millisecond."

Blimey, we might as well pack up and go home then!

Actually I didn't realise people took these things so seriously. I came 
into the thread when I thought it was being suggested that brute-force 
approaches to this problem were not viable.

I think to be useful, it needs to work in a reasonable amount of time, 
and a few seconds would be more than reasonable; it doesn't need to be 
100 microseconds. Unless somehow somebody's got millions of the things 
to get through.

But I guess people aren't interested in actually solving the daily 
sudoku in the paper** (that would be very dull); maybe there is more 
sport in finding a faster machine solution than anyone else.

(I'm more interested now in getting my own dynamic language to compete 
with PyPy, and in getting own static language to compete with C/gcc, as 
the timing for this benchmark was pretty bad.)

(** Although I did come across a prize 16x16 sudoku in the paper a few 
years back. I adapted my code to 16x16 in 10 minutes or so, which took a 
further couple of minutes to solve the given puzzle, and sent it in. But 
I didn't win...)

-- 
Bartc

[toc] | [prev] | [next] | [standalone]

#88301

On Sun, 29 Mar 2015 23:17:23 +0100, BartC <bc@freeuk.com> wrote:

>On 29/03/2015 22:21, Mark Lawrence wrote:
>> On 28/03/2015 23:50, BartC wrote:
>>> On 28/03/2015 03:39, Sayth wrote:
>>>> Good test for pypy to see where it's speed sits between C and Python.
>
>>> Python 3.1:     1700 seconds     (normal Python interpreter)
>>> PyPy:           93 seconds
>>> C unoptimised:  17 seconds       (gcc -O0 32-bit)
>>> C optimised:    3.3 seconds      (gcc -O3 32-bit)
>
>> https://attractivechaos.wordpress.com/2011/06/19/an-incomplete-review-of-sudoku-solver-implementations/
>
>"The fastest Sudoku solver can solve even the hardest Sudoku in about 1 
>millisecond and solve most others in 0.1 millisecond."
>
>Blimey, we might as well pack up and go home then!
>
>Actually I didn't realise people took these things so seriously. I came 
>into the thread when I thought it was being suggested that brute-force 
>approaches to this problem were not viable.
>
>I think to be useful, it needs to work in a reasonable amount of time, 
>and a few seconds would be more than reasonable; it doesn't need to be 
>100 microseconds. Unless somehow somebody's got millions of the things 
>to get through.
>
>But I guess people aren't interested in actually solving the daily 
>sudoku in the paper** (that would be very dull); maybe there is more 
>sport in finding a faster machine solution than anyone else.
>
The technical term for that is "a pissing contest"

>(I'm more interested now in getting my own dynamic language to compete 
>with PyPy, and in getting own static language to compete with C/gcc, as 
>the timing for this benchmark was pretty bad.)
>
>(** Although I did come across a prize 16x16 sudoku in the paper a few 
>years back. I adapted my code to 16x16 in 10 minutes or so, which took a 
>further couple of minutes to solve the given puzzle, and sent it in. But 
>I didn't win...)

[toc] | [prev] | [next] | [standalone]

#87989

On Wed, 25 Mar 2015 10:39 pm, Marko Rauhamaa wrote:

> I have yet to find practical use for fibonacci numbers.

Many people have failed to find practical uses for many things from
mathematics. Doesn't mean they don't exist:

http://en.wikipedia.org/wiki/Fibonacci_number#Applications



-- 
Steven

[toc] | [prev] | [next] | [standalone]

#87990

On 25/03/2015 22:50, Steven D'Aprano wrote:
> On Wed, 25 Mar 2015 10:39 pm, Marko Rauhamaa wrote:
>
>> I have yet to find practical use for fibonacci numbers.
>
> Many people have failed to find practical uses for many things from
> mathematics. Doesn't mean they don't exist:
>
> http://en.wikipedia.org/wiki/Fibonacci_number#Applications
>

I've just read "Alan Turing: The Enigma".  Apparently he was fascinated 
by the appearance of Fibonacci numbers in nature, as described here 
http://en.wikipedia.org/wiki/Fibonacci_number#In_nature

-- 
My fellow Pythonistas, ask not what our language can do for you, ask
what you can do for our language.

Mark Lawrence

[toc] | [prev] | [next] | [standalone]

#88135

Am 26.03.15 um 00:04 schrieb Mark Lawrence:
> On 25/03/2015 22:50, Steven D'Aprano wrote:
>> On Wed, 25 Mar 2015 10:39 pm, Marko Rauhamaa wrote:
>>
>>> I have yet to find practical use for fibonacci numbers.
>>
>> Many people have failed to find practical uses for many things from
>> mathematics. Doesn't mean they don't exist:
>>
>> http://en.wikipedia.org/wiki/Fibonacci_number#Applications
>>
>
> I've just read "Alan Turing: The Enigma".  Apparently he was fascinated
> by the appearance of Fibonacci numbers in nature, as described here
> http://en.wikipedia.org/wiki/Fibonacci_number#In_nature
>
https://xkcd.com/spiral/

[toc] | [prev] | [next] | [standalone]

#88033

"Marko Rauhamaa" <marko@pacujo.net> wrote in message 
news:87r3sdnw5t.fsf@elektro.pacujo.net...
>
>
> I post below a sudoku solver. I eagerly await neater implementations (as
> well as bug reports).
>

Here is another python-based sudoku solver -

http://www.ics.uci.edu/~eppstein/PADS/Sudoku.py

>From its docstring -

"A proper Sudoku puzzle must have a unique solution, and it should be 
possible to reach that solution by a sequence of logical deductions without 
trial and error.  To the extent possible, we strive to keep the same ethic 
in our automated solver, by mimicking human rule-based reasoning, rather 
than resorting to brute force backtracking search."

A neat feature is that, having printed the solution, it then lists every 
step it took in its reasoning process to arrive at the solution.

It solved Marko's original puzzle and Ian's puzzle in less than a second. It 
could not solve Marko's second one, returning "impossible" immediately.

Here is another one that does not use python, but uses SQL -

https://www.sqlite.org/lang_with.html

You will find it at the bottom of the page, under the heading "Outlandish 
Recursive Query Examples".

Frank Millman

[toc] | [prev] | [next] | [standalone]

#88045

"Frank Millman" <frank@chagford.com>:

> Here is another python-based sudoku solver -
>
> http://www.ics.uci.edu/~eppstein/PADS/Sudoku.py
>
>>From its docstring -
>
> "A proper Sudoku puzzle must have a unique solution, and it should be
> possible to reach that solution by a sequence of logical deductions
> without trial and error.

I don't think that statement holds water. Trial-and-error is at the
basis of deduction (reductio ad absurdum). The human solver employs it
in their head. The question is, what is the difference between
pen-and-paper and in-your-head for a computer program?

(Question: Are computers good at blindfold chess?)

> To the extent possible, we strive to keep the same ethic in our
> automated solver, by mimicking human rule-based reasoning, rather than
> resorting to brute force backtracking search."

That's cool...

> A neat feature is that, having printed the solution, it then lists
> every step it took in its reasoning process to arrive at the solution.
>
> It solved Marko's original puzzle and Ian's puzzle in less than a
> second. It could not solve Marko's second one, returning "impossible"
> immediately.

... but that realization greatly reduces the value of the solver.

I brought up sudoku solving as a "real-world" example of the usefulness
of exhaustive recursion. The concerns on astronomical execution times
must be considered but at the same time, one should realize things
aren't as bad as they would seem: exhaustion is a practical way to solve
sudoku puzzles and analogous programming challenges.

The compactness of a working sudoku solver should demonstrate something
about (1) the usefulness of recursion and (2) the expressive power of
Python.


Marko

[toc] | [prev] | [next] | [standalone]

#88046

On Thu, Mar 26, 2015 at 11:26 PM, Marko Rauhamaa <marko@pacujo.net> wrote:
> "Frank Millman" <frank@chagford.com>:
>
>> Here is another python-based sudoku solver -
>>
>> http://www.ics.uci.edu/~eppstein/PADS/Sudoku.py
>>
>>>From its docstring -
>>
>> "A proper Sudoku puzzle must have a unique solution, and it should be
>> possible to reach that solution by a sequence of logical deductions
>> without trial and error.
>
> I don't think that statement holds water. Trial-and-error is at the
> basis of deduction (reductio ad absurdum). The human solver employs it
> in their head. The question is, what is the difference between
> pen-and-paper and in-your-head for a computer program?

Nothing. And solving a Sudoku puzzle - or any other puzzle - should
require no guessing. It should be possible to solve purely by logic.
Same goes for every other kind of puzzle out there; it's highly
unsatisfying to play Minesweeper and get to the end with a block of
four squares in a corner, two mines left, and no way of knowing which
diagonal has the mines and which is clear.

No trial-and-error, thanks.

ChrisA

[toc] | [prev] | [next] | [standalone]

#88050

[Multipart message — attachments visible in raw view] — view raw

On Mar 26, 2015 6:31 AM, "Marko Rauhamaa" <marko@pacujo.net> wrote:
>
> "Frank Millman" <frank@chagford.com>:
>
> > Here is another python-based sudoku solver -
> >
> > http://www.ics.uci.edu/~eppstein/PADS/Sudoku.py
> >
> >>From its docstring -
> >
> > "A proper Sudoku puzzle must have a unique solution, and it should be
> > possible to reach that solution by a sequence of logical deductions
> > without trial and error.
>
> I don't think that statement holds water. Trial-and-error is at the
> basis of deduction (reductio ad absurdum). The human solver employs it
> in their head. The question is, what is the difference between
> pen-and-paper and in-your-head for a computer program?

It's an accurate characterization of the sort of puzzles that are typically
presented as sudoku. I don't think that I have used trial and error, in my
head or otherwise, in any sudoku I have ever solved.

> > It solved Marko's original puzzle and Ian's puzzle in less than a
> > second. It could not solve Marko's second one, returning "impossible"
> > immediately.

Perhaps this is why that puzzle was described as being so difficult: it
required steps that human solvers don't usually take.

[toc] | [prev] | [next] | [standalone]

#88057

Ian Kelly <ian.g.kelly@gmail.com>:

> I don't think that I have used trial and error, in my head or
> otherwise, in any sudoku I have ever solved.

Of course you have. "This here can't be a 2 because if it were a 2, that
there would have to be a 5, which is impossible. Thus, the only
remaining alternative is 3, so I mark that down."

That's trial and error, aka, reductio ad absurdum.

(Additionally, sudoku solvers are known to pencil all kinds of markings
on the sudoku sheets to help the deduction work.)


Marko

[toc] | [prev] | [next] | [standalone]

#88060

On Thu, Mar 26, 2015 at 8:23 AM, Marko Rauhamaa <marko@pacujo.net> wrote:
> Ian Kelly <ian.g.kelly@gmail.com>:
>
>> I don't think that I have used trial and error, in my head or
>> otherwise, in any sudoku I have ever solved.
>
> Of course you have. "This here can't be a 2 because if it were a 2, that
> there would have to be a 5, which is impossible. Thus, the only
> remaining alternative is 3, so I mark that down."
>
> That's trial and error, aka, reductio ad absurdum.
>
> (Additionally, sudoku solvers are known to pencil all kinds of markings
> on the sudoku sheets to help the deduction work.)

Okay, I've probably used single-lookahead trial and error in my
reasoning at some point. But the example you give is equivalent to the
deductive process "That can't be a 5, so I remove it as a candidate.
The only place left for a 5 is here, so I remove the 2 as a candidate
and fill in the 5."

[toc] | [prev] | [next] | [standalone]

#88072

Ian Kelly <ian.g.kelly@gmail.com>:

> On Thu, Mar 26, 2015 at 8:23 AM, Marko Rauhamaa <marko@pacujo.net> wrote:
>> That's trial and error, aka, reductio ad absurdum.
>
> Okay, I've probably used single-lookahead trial and error in my
> reasoning at some point. But the example you give is equivalent to the
> deductive process "That can't be a 5, so I remove it as a candidate.
> The only place left for a 5 is here, so I remove the 2 as a candidate
> and fill in the 5."

In fact, the "trial-and-error" technique is used in automated theorem
proving:

  Lean provers are generally implemented in Prolog, and make proficient
  use of the backtracking engine and logic variables of that language.

  <URL: http://en.wikipedia.org/wiki/Lean_theorem_prover>


Marko

[toc] | [prev] | [next] | [standalone]

#88074

On Thu, Mar 26, 2015 at 9:48 AM, Marko Rauhamaa <marko@pacujo.net> wrote:
> Ian Kelly <ian.g.kelly@gmail.com>:
>
>> On Thu, Mar 26, 2015 at 8:23 AM, Marko Rauhamaa <marko@pacujo.net> wrote:
>>> That's trial and error, aka, reductio ad absurdum.
>>
>> Okay, I've probably used single-lookahead trial and error in my
>> reasoning at some point. But the example you give is equivalent to the
>> deductive process "That can't be a 5, so I remove it as a candidate.
>> The only place left for a 5 is here, so I remove the 2 as a candidate
>> and fill in the 5."
>
> In fact, the "trial-and-error" technique is used in automated theorem
> proving:
>
>   Lean provers are generally implemented in Prolog, and make proficient
>   use of the backtracking engine and logic variables of that language.
>
>   <URL: http://en.wikipedia.org/wiki/Lean_theorem_prover>

Sure, but what has this to do with the statement that *sudoku* should
not require trial and error to solve?

[toc] | [prev] | [next] | [standalone]

#88076

Ian Kelly <ian.g.kelly@gmail.com>:

> On Thu, Mar 26, 2015 at 9:48 AM, Marko Rauhamaa <marko@pacujo.net> wrote:
>> In fact, the "trial-and-error" technique is used in automated theorem
>> proving:
>>
>>   Lean provers are generally implemented in Prolog, and make proficient
>>   use of the backtracking engine and logic variables of that language.
>>
>>   <URL: http://en.wikipedia.org/wiki/Lean_theorem_prover>
>
> Sure, but what has this to do with the statement that *sudoku* should
> not require trial and error to solve?

Trial-and-error was presented in opposition to logical deduction, while
really trial-and-error *is* logical deduction.


Marko

[toc] | [prev] | [next] | [standalone]

#88055

On 03/26/2015 08:37 AM, Chris Angelico wrote:
> On Thu, Mar 26, 2015 at 11:26 PM, Marko Rauhamaa <marko@pacujo.net> wrote:
>> "Frank Millman" <frank@chagford.com>:
>>
>>> Here is another python-based sudoku solver -
>>>
>>> http://www.ics.uci.edu/~eppstein/PADS/Sudoku.py
>>>
>>> >From its docstring -
>>>
>>> "A proper Sudoku puzzle must have a unique solution, and it should be
>>> possible to reach that solution by a sequence of logical deductions
>>> without trial and error.
>>
>> I don't think that statement holds water. Trial-and-error is at the
>> basis of deduction (reductio ad absurdum). The human solver employs it
>> in their head. The question is, what is the difference between
>> pen-and-paper and in-your-head for a computer program?
>
> Nothing. And solving a Sudoku puzzle - or any other puzzle - should
> require no guessing. It should be possible to solve purely by logic.
> Same goes for every other kind of puzzle out there; it's highly
> unsatisfying to play Minesweeper and get to the end with a block of
> four squares in a corner, two mines left, and no way of knowing which
> diagonal has the mines and which is clear.
>
> No trial-and-error, thanks.

I think you're making an unwarranted assumption here.  Your Minesweeper 
example has two solutions, so there's no way of telling which is the 
"correct" one.  But I'd claim that there are puzzles which have exactly 
one solution, but which need trial and error at some point to find that 
solution.

I'm not sure how to prove it, since somebody could claim that I just 
haven't tried all the non-trial-and-error rules.

I did write a Sudoku-solver many years ago, in C++, and it solved the 
typical Sudoku I fed it in about 2ms.  But it was deliberately written 
to apply only rules that humans could readily apply.  No backtracking. 
I did not at that time have any electronic source for puzzles, and I got 
bored with manually entering them in from puzzle books.  So I never 
actually encountered a puzzle it couldn't solve.  I mostly used it to 
determine that a puzzle I couldn't manually solve was in fact uniquely 
solvable, and that I'd just messed up somehow.

I wish I still had that source code, as it probably sounds like I'm 
blowing smoke here.

The general approach I used was to make objects of each of the cells, 
which tracked its neighbors to decide whether its value was determined. 
  And when it was determined, it notified its other neighbors.  In turn, 
if that decided a value for any of the neighbors, that cell notified its 
neighbors.  Likewise each row or column or box kept track of its state 
and notified the appropriate cells whenever something interesting was 
discovered.  Then the outer loop just tickled each cell in turn, and the 
solution rippled out.


Maybe I'm misinterpreting your phrase "No trial and error, thanks". 
Perhaps you're saying that puzzles that require trial and error are no 
fun to solve for humans.  And that's a different matter entirely.  I do 
the daily KenKen puzzles in my local paper, and they're just hard enough 
to be fun, seldom taking longer than I'm willing to take in the mornings.

-- 
DaveA

[toc] | [prev] | [next] | [standalone]

#88058

On Fri, Mar 27, 2015 at 1:14 AM, Dave Angel <davea@davea.name> wrote:
> On 03/26/2015 08:37 AM, Chris Angelico wrote:
>> Nothing. And solving a Sudoku puzzle - or any other puzzle - should
>> require no guessing. It should be possible to solve purely by logic.
>> Same goes for every other kind of puzzle out there; it's highly
>> unsatisfying to play Minesweeper and get to the end with a block of
>> four squares in a corner, two mines left, and no way of knowing which
>> diagonal has the mines and which is clear.
>>
>> No trial-and-error, thanks.
>
>
> I think you're making an unwarranted assumption here.  Your Minesweeper
> example has two solutions, so there's no way of telling which is the
> "correct" one.  But I'd claim that there are puzzles which have exactly one
> solution, but which need trial and error at some point to find that
> solution.

Only one can possibly be correct; if you dig one cell, you'll die, and
if you dig the other, you'll win. But you have no way of knowing which
is which, without dying, using some kind of "undo" feature (orange
smoke comes to mind), and trying the other. Or, of course, guessing
right, in which case you win.

> I'm not sure how to prove it, since somebody could claim that I just haven't
> tried all the non-trial-and-error rules.

With Sudoku, there are some pretty complicated rules and patterns.
Minesweeper is much simpler to prove. But there are still rules and
patterns, and at some point, you simply have to say that a puzzle is
"beyond the logic of this set of rules". It might not be beyond a more
comprehensive set of rules, but that doesn't matter; you've proven the
puzzle to be unsolvable *with your (program's) skill set*.

> I did write a Sudoku-solver many years ago, in C++, and it solved the
> typical Sudoku I fed it in about 2ms.  But it was deliberately written to
> apply only rules that humans could readily apply.  No backtracking. I did
> not at that time have any electronic source for puzzles, and I got bored
> with manually entering them in from puzzle books.  So I never actually
> encountered a puzzle it couldn't solve.  I mostly used it to determine that
> a puzzle I couldn't manually solve was in fact uniquely solvable, and that
> I'd just messed up somehow.
>
> I wish I still had that source code, as it probably sounds like I'm blowing
> smoke here.
>
> The general approach I used was to make objects of each of the cells, which
> tracked its neighbors to decide whether its value was determined.  And when
> it was determined, it notified its other neighbors.  In turn, if that
> decided a value for any of the neighbors, that cell notified its neighbors.
> Likewise each row or column or box kept track of its state and notified the
> appropriate cells whenever something interesting was discovered.  Then the
> outer loop just tickled each cell in turn, and the solution rippled out.

Not entirely sure I have this correct, but it sounds like you have a
basic solver that uses one rule: If there is no other value that can
be in this cell, you can write this one down. It's certainly possible
to add a lot more sophistication to a solver; for instance, in this
grid, it's possible to place a 4 with certainty:

. . . | . . . | . . .
. . . | 4 . . | . . .
. . . | . . . | . . 4
------+-------+------
. . . | . . . | . . .
. . . | . . . | . . .
. . . | . . . | . 4 .
------+-------+------
. . . | . . . | . . .
. . . | . 1 2 | . . .
4 . . | . . . | . . .

An examination of the bottom-center block shows that the 4 in it must
be on its top row (even though you don't know which of two
possibilities has it), ergo the bottom-right block must have its 4 on
the center row. The more of these kinds of rules you have, the more
puzzles you can solve - but I would still code the solver to avoid
guessing.

> Maybe I'm misinterpreting your phrase "No trial and error, thanks". Perhaps
> you're saying that puzzles that require trial and error are no fun to solve
> for humans.  And that's a different matter entirely.  I do the daily KenKen
> puzzles in my local paper, and they're just hard enough to be fun, seldom
> taking longer than I'm willing to take in the mornings.

I agree that they're no fun for humans. That's part of the point, but
not the whole point. Since we're talking about puzzles, here, the
primary purpose of a machine solver is (or should be!) to prove that a
puzzle is solvable, and thus worthy of being given to a human. So the
solver should restrict itself to what's considered worth working with
- and in some cases, might restrict itself even further ("generate an
easy puzzle, please"), by cutting out some forms of logic. Now, if
your humans are happy with puzzles that they have to guess, then sure,
incorporate guessing in your solver. But if the humans aren't, then
what do you prove by having an electronic solver that can do the
puzzle? There's a small mathematical curiosity to finding out just how
few clues can carry sufficient information to uniquely define a grid,
but that's already been proven. So, that's why I would avoid guessing.

I've written a lot of solvers for various puzzles. Minesweeper,
Sudoku, a binary Sudoku-like puzzle that I don't really have a good
name for, several others. Every time, I've tried to prove the puzzles
solvable by humans, and sometimes that means rejecting ones that could
technically be solved by brute force.

ChrisA

[toc] | [prev] | [next] | [standalone]

#88059

On 03/26/2015 10:41 AM, Chris Angelico wrote:
  that's already been proven. So, that's why I would avoid guessing.
>
> I've written a lot of solvers for various puzzles. Minesweeper,
> Sudoku, a binary Sudoku-like puzzle that I don't really have a good
> name for, several others. Every time, I've tried to prove the puzzles
> solvable by humans, and sometimes that means rejecting ones that could
> technically be solved by brute force.

OK, we're on the same page.  I would use different terminology for some 
of it, but that's okay.

The purist in me would like to write a solver which (within a few 
seconds) could solve any unique puzzle, and identify puzzles which don't 
have a unique solution.  One reason I never got back to writing one was 
I also wanted a difficulty-ranker, which would identify how hard a human 
was likely to consider the puzzle.

Had I been writing it in Python, I'd probably have pursued adding brute 
force, and then used some of the code to write a puzzle-generator.  But 
even then, the problem of ranking was one that had me buffaloed.  It's 
clearly not enough to count the starting clues

(eg. easyness = (clues - 17) * pi )

And writing an efficient program that generates a non-trivial puzzle 
would seem to be quite hard.  I've heard it said that Sudoku puzzles 
generated by machines are much less satisfying than those generated by a 
human.

When in a playful mood, I wonder if all the Sudoku puzzles out there are 
just permutations of a few hundred written by Will Shortz.  Swap around 
rows, columns, boxes, and cryptogram the digit mapping.  Voila, a new 
puzzle.  <g>  i read a short story about the purpose of jokes, in which 
it said there were only a few hundred of them, the rest were just minor 
variants, and that they were an experiment being run on human beings. 
And once we realized it, they'd shut off our sense of humor.

-- 
DaveA

[toc] | [prev] | [next] | [standalone]

#88071

Dave Angel <davea@davea.name>:

> When in a playful mood, I wonder if all the Sudoku puzzles out there
> are just permutations of a few hundred written by Will Shortz.

A sudoku solver can be trivially turned into a puzzle generator:

========================================================================
$ ./sudoku.py --generate >puzzle.dat
$ cat puzzle.dat
3 . 2 . 4 . . . .
4 5 . . . 6 . . .
6 . . . 9 . . 8 .
. . . . . . 5 . .
. 6 4 . . 9 . 3 .
. 7 3 5 . . . 4 8
. . . . . . 8 . .
. 8 . . 7 . . . 3
. . . . 1 . . . 2

$ ./sudoku.py <puzzle.dat 
3 9 2 8 4 7 1 6 5
4 5 8 1 3 6 7 2 9
6 1 7 2 9 5 3 8 4
8 2 1 4 6 3 5 9 7
5 6 4 7 8 9 2 3 1
9 7 3 5 2 1 6 4 8
1 4 9 3 5 2 8 7 6
2 8 5 6 7 4 9 1 3
7 3 6 9 1 8 4 5 2

========================================================================

========================================================================
#!/usr/bin/env python3

import sys, random

M = 3
N = M * M
P = M * N
Q = M * P

EMPTY = "."

buddies = [ [ buddy
              for buddy in range(Q)
              if buddy != slot and
                  (buddy % N == slot % N or
                   buddy // N == slot // N or
                   buddy // P == slot // P and
                   buddy % N // M == slot % N // M) ]
            for slot in range(Q) ]
interned = { n : n for n in range(1, N + 1) }
candidates = list(interned.values())

def main():
    if len(sys.argv) > 1 and sys.argv[1] == "--generate":
        generate()
        return
    board = []
    for n in sys.stdin.read().split():
        try:
            board.append(int(n))
        except ValueError:
            board.append(EMPTY)
    for solution in solve(board):
        report(solution)

def generate():
    report(minimize(next(solve([ EMPTY ] * Q))))

def solve(board, slot=0):
    if slot == Q:
        yield board[:]
    elif board[slot] is EMPTY:
        shuffled = candidates[:]
        random.shuffle(shuffled)
        for candidate in shuffled:
            for buddy in buddies[slot]:
                if board[buddy] is candidate:
                    break
            else:
                board[slot] = candidate
                yield from solve(board, slot + 1)
        board[slot] = EMPTY
    else:
        yield from solve(board, slot + 1)

def minimize(board):
    while True:
        nonempty_slots = [ slot for slot in range(Q)
                           if board[slot] is not EMPTY ]
        random.shuffle(nonempty_slots)
        for slot in nonempty_slots:
            removed, board[slot] = board[slot], EMPTY
            if uniquely_solvable(board):
                break
            board[slot] = removed
        else:
            return board

def uniquely_solvable(board):
    it = solve(board[:])
    next(it)
    try:
        next(it)
    except StopIteration:
        return True
    return False

def report(board):
    print("\n".join(
        " ".join(str(board[row * N + col])
                 for col in range(N))
        for row in range(N)))
    print()

if __name__ == '__main__':
    main()
========================================================================


Marko

[toc] | [prev] | [next] | [standalone]

Page 3 of 5 — ← Prev page 1 2 [3] 4 5  Next page →

Back to top | Article view | comp.lang.python

csiph-web