n-Queens problem possible solutions by logical equivalences I'm studying Discrete maths recently, mainly through MIT 6042J and Rosen's Discrete Math and its applications.
In the later, I found the following problem I can't figure out how to proceed:
The context is the well-known n-Queens problem and on the textbook, the following compound preposition is given:
Let $p(i,j)$ be a proposition that is $True$ iff there's a queen in the $i$th row and $j$th column, where $i = 1...n$ and $j = 1...n$.

*

*to check all row contains at least one queen: $Q_1 = \land_{i=1}^n\lor_{j=1}^np(i,j)$

*to check at most one queen per row: $Q_2 = \land_{i=1}^n\land_{j=1}^{n-1}\land_{k=j+1}^n(\lnot p(i,j)\lor\lnot p(k,j))$

*

*Here comes my first question. I believe it's wrong and should be $Q_2 = \land_{i=1}^n\land_{j=1}^{n-1}\land_{k=j+1}^n(\lnot p(i,j)\lor\lnot p(\textbf{i,k}))$ but I couldn't find any public errata. Does it make sense?



*to check at most one queen per column: $Q_3 = \land_{j=1}^n\land_{i=1}^{n-1}\land_{k=i+1}^n(\lnot p(i,j)\lor\lnot p(k,j))$

*to assert at most one queen on the diagonals:

*

*$Q_4 = \land_{i=2}^n\land_{j=1}^{n-1}\land_{k=1}^{min(i-1,n-j)}(\lnot p(i,j)\lor\lnot p(i-k,k+j))$

*$Q_5 = \land_{i=1}^{n-1}\land_{j=1}^{n-1}\land_{k=1}^{min(n-i,n-j)}(\lnot p(i,j)\lor\lnot p(i+k,j+k))$
So, to find valid results we need: $Q = Q_1 \land Q_2 \land Q_3 \land Q_4 \land Q_5$
I understand all of the proposed compound propositions and how they work. I could even easily convert them into an algorithm.
But the proposed exercises ask us to use them to find all the possible solutions for $n=4$. There are 65536 combinations for that, so, my second and final question is: is it possible to reduce these compounds with logic equivalences and, I'm not seeing it, or is it more probable that the book expects a computational solution for that?
Thanks in advance.
 A: Instead of testing all $4^{4\times 4}$ possibilities, you can do some backtracking/lazy evaluation.
Start by placing a queen in the first column, up to symetries there is only $2$ possible positions, $p(1,1)$ and $p(1,2)$, draw the two and start to explore the $p(1,1)$ branch.
This first queen induces a lot of constraints, we draw them in green and see that we have 2 possibilities for the placement of the second queen: $p(2,3)$ and $p(2,4)$. We draw these two configuration and carry on exploring the $p(1,1), p(2,3)$ branch.
Now, adding in red the constraints induced by the second queen and previously unconstrained, we see that there is no way to place a non-attacking queen in the third column, so we stop our exploration and go back to the next unexplored branch, $p(1,1),p(2,4)$.
Here we can put a non-attacking queen at $p(3,2)$ and carry on.
I won't describe the whole process, I think my drawing is way clearer.

We end up with one suitable configuration $p(1,2),p(2,4),p(3,1), p(4,3)$, and we have to keep in mind that we used symmetry to simplify one half of the computations so $p(1,3),p(2,1),p(3,4),p(4,2)$ works as well.
Hence we have $2$ possibles configurations, this is coherent with http://oeis.org/A000170
I described the process manually, but it is also very suitable for computer programming. It also works in your logical framework, by doing the lazy evaluation of your $\wedge$ (which is $False$ as soon as one proposition is).
https://en.wikipedia.org/wiki/Backtracking
