The nxn queens problem is if the is a solution where n queens can exists on a nxn board with the rules of chess, 1 per row,col,diagonal. I am trying to represent the nxn queens problem where n=3 in propositional form. so we define 9 Boolean variables, let a,b,c, represent the entries on row 1, d,e,f the entries on row 2, and g,h,i represent the entires on row 3. So given the rules we have the following propositional formula:
Exactly one queen on top row : (a∨b∨c) ∧ ~( a∧b∧c)
Exactly one queen on middle row : (d∨e∨f) ∧ ~( d∧e∧f)
Exactly one queen on bottom row: (g∨h∨i) ∧ ~( g∧h∧i)
Exactly one queen on left column : (a∨d∨g) ∧ ~( a∧d∧g)
Exactly one queen one queen on middle column : (b∨d∨h) ∧ ~( b∧d∧h)
Exactly one queen on right column: (c∨e∨i) ∧ ~( c∧e∧i)
No two queens on the same diagonal: ~(a∨e∨i) ∧ ~( c∧e∧d)
However, this returns satisfiable on the sat solver, yet we know that the nxn queens problem is only solvable for n>3, so my representation must be false.
This is wrong, as it still allows two queens in the same row
So do:
$$(a \lor b \lor c) \land \neg (a \land b) \land \neg (a \land c) \land \neg (b \land c)$$
... same for the others ...