Tower diagram - logic expression? (queen problem) I have given a square which consists of $n \times n$ fields.
I must formulate logical expressions which say:
1) In every row there is $0$ or $1$ tower.
2) In every column there is $0$ or $1$ tower.
For example like this:
-------
|T| | |
-------
| | |T|
-------
| |T| |
-------

I know how to formulate (1) for, say, $3 \times 3$ (let $A_{i,j}$ be true if there is a tower on the field):
$(A_{1,1} \land \lnot A_{1,2} \land \lnot A_{1,3}) \lor$ 
$(\lnot A_{1,1} \land A_{1,2} \land \lnot A_{1,3}) \lor$ 
$(\lnot A_{1,1} \land \lnot A_{1,2} \land  A_{1,3}) $ (Row 1)
$(A_{2,1} \land \lnot A_{2,2} \land \lnot A_{2,3}) \lor$ 
$(\lnot A_{2,1} \land A_{2,2} \land \lnot A_{2,3}) \lor$ 
$(\lnot A_{2,1} \land \lnot A_{2,2} \land  A_{2,3}) $ (Row 2)
$(A_{3,1} \land \lnot A_{3,2} \land \lnot A_{3,3}) \lor$ 
$(\lnot A_{3,1} \land A_{3,2} \land \lnot A_{3,3}) \lor$ 
$(\lnot A_{3,1} \land \lnot A_{3,2} \land  A_{3,3}) $ (Row 3)
2) Works very similar...but how can I say that in general?
 A: This is a partial solution, which satisfies conditions 1 and 2 only in part, i.e. the logic expression says that there is at least one tower and at least one absence of a tower in each row and column. I hope this will give you enough of an idea, in terms of approach, to extend it to the at most 1 tower case.
However, I suspect that once the conditions at least one tower and at least one absence of a tower are satisfied by all rows and columns, you're left with one, and only one tower per each row and column, i.e. $n$ towers on a $n\times n$ grid. This seems right since that's the solution to the Queens Problem.
Conditions 1 and 2 can be simplified with an expression that is logically equivalent to the disjunctions of conjuncts that you gave for the $3 \times3$ case. Observe that for each row, conditions 1 and 2 are satisfied if we say that (i) the disjunction of all row elements is true, and (ii) the conjunction of all the row elements is false (or equivalently for (ii), the disjunction of all negated row elements is true, which means that at least one negated row element is true). 
This is so because by definition of disjunction (i) forces it to be the case that there's at least one "tower" (using your definition) in the row, i.e. in row $i$, $A_{i,j}$ is true for at least one $j$, and (ii) puts a restriction by ensuring that $A_{i,k}$ is false for at least one $k$ (obviously $j\not=k$). 
Note that  (ii) could also be expressed as a disjunction of negated statements, i.e. $\lnot A_{i,k}$ is true for at least one $k$ (this is what I give in the example below).
EXAMPLE: For the $3\times3$ case, each row $i$ must satisfy the following condition: 
$$\left ( \underset{j=1}{\overset{3}{\LARGE\lor}}A_{i,j}\right ) \land \left(\underset{j=1}{\overset{3}{\LARGE\lor}}\lnot A_{i,j}\right )$$
And each column $j$ must satisfy the following condition:
$$\left ( \underset{i=1}{\overset{3}{\LARGE\lor}}A_{i,j}\right ) \land \left(\underset{i=1}{\overset{3}{\LARGE\lor}}\lnot A_{i,j}\right )$$
The expression that satisfies 1 and 2 for rows in the general $n\times n$ case is the following (the conjunction at the front makes sure that conditions 1 and 2 hold for each row): $$ \underset{i=1}{\overset{n}{\LARGE\land}} \left[ \left ( \underset{j=1}{\overset{n}{\LARGE\lor}}A_{i,j}\right ) \land \left(\underset{j=1}{\overset{n}{\LARGE\lor}}\lnot A_{i,j}\right )\right]$$
For columns the expression in the general $n\times n$ case is going to be basically identical, with the difference that indices in the conjunction at the front ranges over all columns, and the inner expressions range, for each column, over all rows.
$$ \underset{j=1}{\overset{n}{\LARGE\land}} \left[ \left ( \underset{i=1}{\overset{n}{\LARGE\lor}}A_{i,j}\right ) \land \left(\underset{i=1}{\overset{n}{\LARGE\lor}}\lnot A_{i,j}\right )\right]$$
Putting the two together yields the necessary condition for the entire matrix/square/table:
$$\left [ \underset{i=1}{\overset{n}{\LARGE\land}} \left[ \left ( \underset{j=1}{\overset{n}{\LARGE\lor}}A_{i,j}\right ) \land \left(\underset{j=1}{\overset{n}{\LARGE\lor}}\lnot A_{i,j}\right )\right] \right ] \land \left [ \underset{j=1}{\overset{n}{\LARGE\land}} \left[ \left ( \underset{i=1}{\overset{n}{\LARGE\lor}}A_{i,j}\right ) \land \left(\underset{i=1}{\overset{n}{\LARGE\lor}}\lnot A_{i,j}\right )\right] \right ]$$
Although I suspect that a FOL expression would be much simpler.
