Peaceable Armies of Queens - Revision history

Michael Leuschel at 16:33, 27 January 2021

2021-01-27T16:33:02Z

← Older revision		Revision as of 16:33, 27 January 2021
Line 50:		Line 50:
	</pre>		</pre>

	Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [[Using_ProB_with_KODKOD \| Kodkod as ProB's backend]] and using an [~~http~~://~~alloy~~.~~mit.edu/alloy/~~ Alloy] model (see below).		Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [[Using_ProB_with_KODKOD \| Kodkod as ProB's backend]] and using an [https://alloytools.org Alloy] model (see below).
	<pre>		<pre>
	dim=7, n=7 : solved in 0.3 secs		dim=7, n=7 : solved in 0.3 secs
Line 67:		Line 67:
	=== The Alloy model for comparison ===		=== The Alloy model for comparison ===

	Here is the [~~http~~://~~alloy~~.~~mit.edu/alloy/~~ Alloy] model we have used.		Here is the [https://alloytools.org Alloy] model we have used.
	Initially, the model gave us wrong solutions as we were using <tt>+</tt> instead of <tt>sum</tt>; this was correct for previous versions of Alloy but not for Alloy 4.2 which we were using.		Initially, the model gave us wrong solutions as we were using <tt>+</tt> instead of <tt>sum</tt>; this was correct for previous versions of Alloy but not for Alloy 4.2 which we were using.

Michael Leuschel at 07:58, 27 June 2014

2014-06-27T07:58:59Z

← Older revision		Revision as of 07:58, 27 June 2014
Line 1:		Line 1:
	I found this challenging constraint programming problem in the following paper:		I found this challenging constraint programming problem in the following paper:
	* B. M. Smith, K. E. Petrie, and I. P. Gent. Models and symmetry breaking for peaceable armies of queens. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pages 271–286. Springer Berlin Heidelberg, 2004.		* B. M. Smith, K. E. Petrie, and I. P. Gent. Models and symmetry breaking for peaceable armies of queens. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pages 271–286. Springer Berlin Heidelberg, 2004.
	A variation of the problem can be found on page 329 of the Handbook on Constraint ~~programming~~.		A variation of the problem can be found on page 329 of the [https://www.elsevier.com/books/handbook-of-constraint-programming/rossi/978-0-444-52726-4 Handbook on Constraint Programming].

	The challenge is to place two equal-sized armies of white and black queens onto a chessboard.		The challenge is to place two equal-sized armies of white and black queens onto a chessboard.

Michael Leuschel at 07:57, 27 June 2014

2014-06-27T07:57:16Z

← Older revision		Revision as of 07:57, 27 June 2014
Line 6:		Line 6:
	We can distinguish between two problems:		We can distinguish between two problems:
	* <em>checking</em> whether two armies of <b>n</b> queens can be placed on a <b>dim*dim</b> chessboard,		* <em>checking</em> whether two armies of <b>n</b> queens can be placed on a <b>dim*dim</b> chessboard,
	* for a ~~give~~ board of size <b>dim*dim</b> find the maximal size <b>n</b> of armies that can be placed onto the board, i.e., solving an <em>optimisation</em> problem.		* for a given board of size <b>dim*dim</b> find the maximal size <b>n</b> of armies that can be placed onto the board, i.e., solving an <em>optimisation</em> problem.

	== Checking ==		== Checking ==

Michael Leuschel at 15:55, 20 February 2014

2014-02-20T15:55:25Z

← Older revision		Revision as of 15:55, 20 February 2014
Line 10:		Line 10:
	== Checking ==		== Checking ==
	Here is a B model for the checking problem. The problem is quite straightforward to encode in B.		Here is a B model for the checking problem. The problem is quite straightforward to encode in B.
	Many lines below (in the DEFINITIONS) just define the animation function to graphically represent solutions.		Many lines below (in the DEFINITIONS) just define the [[Graphical_Visualization\|animation function to graphically represent solutions]].

	<pre>		<pre>

Michael Leuschel: /* Checking */

2014-01-25T07:16:45Z

Checking

← Older revision		Revision as of 07:16, 25 January 2014
Line 50:		Line 50:
	</pre>		</pre>

	Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [[Using_ProB_with_KODKOD Kodkod as ProB's backend]] and using an [http://alloy.mit.edu/alloy/ Alloy] model (see below).		Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [[Using_ProB_with_KODKOD \| Kodkod as ProB's backend]] and using an [http://alloy.mit.edu/alloy/ Alloy] model (see below).
	<pre>		<pre>
	dim=7, n=7 : solved in 0.3 secs		dim=7, n=7 : solved in 0.3 secs

Michael Leuschel at 07:16, 25 January 2014

2014-01-25T07:16:05Z

← Older revision		Revision as of 07:16, 25 January 2014
Line 50:		Line 50:
	</pre>		</pre>

	Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [Using_ProB_with_KODKOD Kodkod as ProB's backend] and using an [[http://alloy.mit.edu/alloy/ Alloy]] model (see below).		Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [[Using_ProB_with_KODKOD Kodkod as ProB's backend]] and using an [http://alloy.mit.edu/alloy/ Alloy] model (see below).
	<pre>		<pre>
	dim=7, n=7 : solved in 0.3 secs		dim=7, n=7 : solved in 0.3 secs
Line 67:		Line 67:
	=== The Alloy model for comparison ===		=== The Alloy model for comparison ===

	Here is the [[http://alloy.mit.edu/alloy/ Alloy]] model we have used.		Here is the [http://alloy.mit.edu/alloy/ Alloy] model we have used.
	Initially, the model gave us wrong solutions as we were using <tt>+</tt> instead of <tt>sum</tt>; this was correct for previous versions of Alloy but not for Alloy 4.2 which we were using.		Initially, the model gave us wrong solutions as we were using <tt>+</tt> instead of <tt>sum</tt>; this was correct for previous versions of Alloy but not for Alloy 4.2 which we were using.

Michael Leuschel: /* Optimization */

2014-01-25T07:11:40Z

Optimization

← Older revision		Revision as of 07:11, 25 January 2014
Line 121:		Line 121:

	ProB solves this optimisation problem in about 780 seconds for a board size of 8.		ProB solves this optimisation problem in about 780 seconds for a board size of 8.
			This is very competitive with the timings reported in the above mentioned constraint solving paper using new symmetry breaking techniques and much more low-level encoding on state of the art constraint solving libraries such as ILOG.

	<pre>		<pre>

Michael Leuschel: /* Optimization */

2014-01-25T07:08:03Z

Optimization

← Older revision		Revision as of 07:08, 25 January 2014
Line 124:		Line 124:
	<pre>		<pre>
	MACHINE JustQueens_FindOptimal_CBC		MACHINE JustQueens_FindOptimal_CBC
	/*
	~~dim=5 --> optimum n=4 found in 0.18 secs~~
	~~dim=6 --> optimum n=5 found in 1.16 secs~~
	~~dim=7 --> optimum n=7 found in 21.174 secs~~
	~~dim=8 --> optimum n=9 found in 780.130 secs~~
	*/

	DEFINITIONS		DEFINITIONS
	SET_PREF_TIME_OUT == 1000000;		SET_PREF_TIME_OUT == 1000000;

Michael Leuschel at 07:07, 25 January 2014

2014-01-25T07:07:43Z

@@ Line 50: / Line 50: @@
 </pre>
-Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [Using_ProB_with_KODKOD Kodkod as ProB's backend] and using an Alloy model (see below).
+Here are some running times on my MacBook Air 1.7 GHz i7, also comparing to using [Using_ProB_with_KODKOD Kodkod as ProB's backend] and using an [[http://alloy.mit.edu/alloy/ Alloy]] model (see below).
 <pre>
   dim=7, n=7 : solved in 0.3 secs
@@ Line 60: / Line 60: @@
   dim=8, n=10 : unsat in 728 secs    (Alloy & miniSat still running after over four hours)
 </pre>
 === The Alloy model for comparison ===
 <pre>
 abstract sig Queens {
@@ Line 105: / Line 113: @@
 run valid for 16 Queens, 7 int
 </pre>
 == Optimization ==

Michael Leuschel at 06:59, 25 January 2014

2014-01-25T06:59:52Z

@@ Line 1: / Line 1: @@
 I found this challenging constraint programming problem in the following paper:
 * B. M. Smith, K. E. Petrie, and I. P. Gent. Models and symmetry breaking for peaceable armies of queens. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pages 271–286. Springer Berlin Heidelberg, 2004.
 The challenge is to place two equal-sized armies of white and black queens onto a chessboard.
 We can distinguish between two problems:
-* checking whether two armies of <b>n</b> queens can be placed on a <b>dim*dim</b> chessboard,
+* <em>checking</em> whether two armies of <b>n</b> queens can be placed on a <b>dim*dim</b> chessboard,
-* for a give board of size <b>dim*dim</b> find the maximal size <b>n</b> of armies that can be placed onto the board.
+* for a give board of size <b>dim*dim</b> find the maximal size <b>n</b> of armies that can be placed onto the board, i.e., solving an <em>optimisation</em> problem.
 == Checking ==
 <pre>
 MACHINE JustQueens
 DEFINITIONS
        SET_PREF_TIME_OUT == 1000000;
@@ Line 47: / Line 40: @@
   ORDERED(blackc,blackr) &  /* ensures proper ordering + that we do not place two queens on same square */
   ORDERED(whitec,whiter) &
   !(i,j).(i:1..n & j:1..n => blackc(i) /= whitec(j)) &
@@ Line 58: / Line 50: @@
 </pre>
 == Optimization ==