% prob_queens.pi (in Picat, by Neng-Fa Zhou, June 2014) % A sample ProB model is available at http://www.stups.uni-duesseldorf.de/ProB/index.php5/User_Manual % The following comment is from the original ProB model. /* 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. A variation of the problem can be found on page 329 of the Handbook on Constraint programming. 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 n queens can be placed on a dim*dim chessboard, for a give board of size dim*dim find the maximal size n of armies that can be placed onto the board, i.e., solving an optimisation problem. Checking 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. One can obviously use the above models to try and manually find a maximal value of n for a given board size dim. Below, we have encoded this process as B constraints, by setting up the problem twice: once for the army size n and a second time for army size n+1. The second encoding is wrapped into a negated existential quantification. (This model can no longer be translated into Kodkod because of this.) 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. */ import sat. main => black_white(8,M), writeln(M). black_white(N,M) => QW = new_array(N,N), % White queens QB = new_array(N,N), % Black queens QW :: 0..1, QB :: 0..1, M :: 1..N, sum([QW[I,J] : I in 1..N, J in 1..N]) #= M, sum([QB[I,J] : I in 1..N, J in 1..N]) #= M, foreach(I in 1..N, J in 1..N, I1 in 1..N, J1 in 1..N) if (I==I1 || J==J1 || I+J==I1+J1 || I-J == I1-J1) then QB[I,J] #=> #~ QW[I1,J1] end end, solve([\$max(M)],(QB,QW)), println(\$white([\$pos(I,J) : I in 1..N, J in 1..N, QW[I,J]==1])), println(\$white([\$pos(I,J) : I in 1..N, J in 1..N, QB[I,J]==1])).