queens problem solution

2008-07-24T00:01:00.000-07:00

Hi guys ,
i would like to share my experience while i was part of MSR summer school in Bangalore. It was really fun and challenging to be part of that great community of people. I was one of the 14 B.tech students selected for Summer school from all over world . It was really a great opportunity for me to learn new things especially in field of programming languages, verification and analysis. Researchers and Professors from different part of worlds have come to share their knowledge to us. I am really thankful to all the faculties and organizer committee of summer school program.
We have been given lots of problem to solve in summer school and one of the them was the classical n-queens puzzle is to place n queens on an n × n chess-board so that no two queens attack each other. The exercise asks you to encode an n queens placement problem and then have Z3 enumerate solutions.

Solution to the problem as follows :

(benchmark nqueens
:logic QF_BV
:extrafuns ( (r1 BitVec[8]) (r2 BitVec[8])
(r3 BitVec[8])
(r4 BitVec[8])
(r5 BitVec[8])
(r6 BitVec[8])
(r7 BitVec[8])
(r8 BitVec[8])
)
:formula (and

;Row Constraints
(= bv0[8] (bvand r1 (bvsub r1 bv1[8])))
(= bv0[8] (bvand r2 (bvsub r2 bv1[8])))
(= bv0[8] (bvand r3 (bvsub r3 bv1[8])))
(= bv0[8] (bvand r4 (bvsub r4 bv1[8])))
(= bv0[8] (bvand r5 (bvsub r5 bv1[8])))
(= bv0[8] (bvand r6 (bvsub r6 bv1[8])))
(= bv0[8] (bvand r7 (bvsub r7 bv1[8])))
(= bv0[8] (bvand r8 (bvsub r8 bv1[8])))

; Column Constraints
(not (= bv0[8] r1))(not (= r1 r2) ) (not (= r1 r3) )(not (= r1 r4) )(not (= r1 r5) )(not (= r1 r6) )(not (= r1 r7) )(not (= r1 r8) )
(not (= bv0[8] r2))(not (= r2 r3) ) (not (= r2 r4) )(not (= r2 r5) )(not (= r2 r6) )(not (= r2 r7) )(not (= r2 r8) )
(not (= bv0[8] r3))(not (= r3 r4) )(not (= r3 r5) )(not (= r3 r6) )(not (= r3 r7) )(not (= r3 r8) )
(not (= bv0[8] r4))(not (= r4 r5) )(not (= r4 r6) )(not (= r4 r7) )(not (= r4 r8) )
(not (= bv0[8] r5))(not (= r5 r6) )(not (= r5 r7) )(not (= r5 r8) )
(not (= bv0[8] r6))(not (= r6 r7) )(not (= r6 r8) )
(not (= bv0[8] r7))(not (= r7 r8))
(not (= bv0[8] r8))

; Diagonal Constraints

(not (= r1 (bvshl r2 bv1[8]))) (not (= r1 (bvshl r3 bv2[8]))) (not (= r1 (bvshl r4 bv3[8]))) (not (= r1 (bvshl r5 bv4[8]))) (not (= r1 (bvshl r6 bv5[8]))) (not (= r1 (bvshl r7 bv6[8]))) (not (= r1 (bvshl r8 bv7[8])))
(not (= r1 (bvlshr r2 bv1[8]))) (not (= r1 (bvlshr r3 bv2[8]))) (not (= r1 (bvlshr r4 bv3[8]))) (not (= r1 (bvlshr r5 bv4[8]))) (not (= r1 (bvlshr r6 bv5[8]))) (not (= r1 (bvlshr r7 bv6[8]))) (not (= r1 (bvlshr r8 bv7[8])))
(not (= r2 (bvshl r3 bv1[8]))) (not (= r2 (bvshl r4 bv2[8]))) (not (= r2 (bvshl r5 bv3[8]))) (not (= r2 (bvshl r6 bv4[8]))) (not (= r2 (bvshl r7 bv5[8]))) (not (= r2 (bvshl r8 bv6[8])))
(not (= r2 (bvlshr r3 bv1[8]))) (not (= r2 (bvlshr r4 bv2[8]))) (not (= r2 (bvlshr r5 bv3[8]))) (not (= r2 (bvlshr r6 bv4[8]))) (not (= r2 (bvlshr r7 bv5[8]))) (not (= r2 (bvlshr r8 bv6[8])))
(not (= r3 (bvshl r4 bv1[8]))) (not (= r3 (bvshl r5 bv2[8]))) (not (= r3 (bvshl r6 bv3[8]))) (not (= r3 (bvshl r7 bv4[8]))) (not (= r3 (bvshl r8 bv5[8])))
(not (= r3 (bvlshr r4 bv1[8]))) (not (= r3 (bvlshr r5 bv2[8]))) (not (= r3 (bvlshr r6 bv3[8]))) (not (= r3 (bvlshr r7 bv4[8]))) (not (= r3 (bvlshr r8 bv5[8])))
(not (= r4 (bvshl r5 bv1[8]))) (not (= r4 (bvshl r6 bv2[8]))) (not (= r4 (bvshl r7 bv3[8]))) (not (= r4 (bvshl r8 bv4[8])))
(not (= r4 (bvlshr r5 bv1[8]))) (not (= r4 (bvlshr r6 bv2[8]))) (not (= r4 (bvlshr r7 bv3[8]))) (not (= r4 (bvlshr r8 bv4[8])))
(not (= r5 (bvshl r6 bv1[8]))) (not (= r5 (bvshl r7 bv2[8]))) (not (= r5 (bvshl r8 bv3[8])))
(not (= r5 (bvlshr r6 bv1[8]))) (not (= r5 (bvlshr r7 bv2[8]))) (not (= r5 (bvlshr r8 bv3[8])))
(not (= r6 (bvshl r7 bv1[8]))) (not (= r6 (bvshl r8 bv2[8])))
(not (= r6 (bvlshr r7 bv1[8]))) (not (= r6 (bvlshr r8 bv2[8])))
(not (= r7 (bvshl r8 bv1[8])))
(not (= r7 (bvlshr r8 bv1[8])))

)
)