8 Queens problem

[Javier Soto]

I am slowly working through the 8 Queens problem. I have the gist of it (I think), which is to create a constraint that: given a list of cells, makes sure there is a single Queen (or none) in the list. That way I can define rows, cols and diagonals and enforce the constraint on all of them.

The problem is that besides rotations of the board, I have solutions of boards with 0 queens, boards with a  single queen in different positions, with 2, etc, up to 8. A big mess. I need to make a constraint that forces the total number of queens in the board to be exactly 8. It is easy for 0 or 1, but for anything higher I need the ability to count.

I am assuming that each cell in the board is a fresh variable. So the board is a list of n x n fresh variables.

The Queen is nothing but a value 'Q, and each cell (fresh var) can be unified with 'Q or '_ (empty) using condes.

My hurdle is to create a constraint that says, given a list with all the cells (the board), succeed only if there are exactly 8 queens in it. 

Any ideas of how to count the number of 'Q in a given list of fresh variables?

Thanks,

Javier

[Ryan Davis]

> On Jul 12, 2015, at 18:42, Javier Soto <sotos...@gmail.com> wrote:
>
> I am slowly working through the 8 Queens problem. I have the gist of it (I think), which is to create a constraint that: given a list of cells, makes sure there is a single Queen (or none) in the list. That way I can define rows, cols and diagonals and enforce the constraint on all of them.
>
> The problem is that besides rotations of the board, I have solutions of boards with 0 queens, boards with a single queen in different positions, with 2, etc, up to 8. A big mess. I need to make a constraint that forces the total number of queens in the board to be exactly 8. It is easy for 0 or 1, but for anything higher I need the ability to count.

Not necessarily. You can treat the positional information as purely symbolic.

> I am assuming that each cell in the board is a fresh variable. So the board is a list of n x n fresh variables.
> The Queen is nothing but a value 'Q, and each cell (fresh var) can be unified with 'Q or '_ (empty) using condes.
>
> My hurdle is to create a constraint that says, given a list with all the cells (the board), succeed only if there are exactly 8 queens in it.

This should be easy enough:

Given a list (row or column), cons° to extract a/d, if a is 'q, the rest must all be null (aka, use cond-a and if you see another queen then %u), otherwise recurse on d.

> Any ideas of how to count the number of 'Q in a given list of fresh variables?

Not sure you need to count, just that you need to ensure that there's only 1 'Q, not that there isn't 2+.

I'm currently going with peano numbers '() == 0, '(()) == 1, etc. Since I only need to increment / decrement with my current algorithm, it seemed easier than dealing with Oleg numbers. However, I'm having exponential growth problems:

1: cpu time: 1 real time: 1 gc time: 0
4: cpu time: 6 real time: 7 gc time: 0
6: cpu time: 1709 real time: 1721 gc time: 38
8: ?? heat death?

HEY! It just finished as I was typing this...

8: cpu time: 858264 real time: 864061 gc time: 13760

ouch...

[Javier Soto]

Ok, I finally did it. I get 92 solutions of the 8Queens problems which involve all rotations and reflections of the unique 12 solutions. 

My approach takes 36 seconds. 

But,.... yes... I cheated! because my solutions cannot be generalized to other boards (like 9x9, etc).

I analyzed the final 12 solutions and derived some insights that allowed me to narrow the problem. (Actually, I wonder if I could actually generalize those insights for bigger boards... uhm), whatever, I look forward to other people's approaches or ways to apply MiniKanren to weird things.

J