# Four Queens Problem to a Conjunctive Normal Form

Given a chessboard with 4 rows and 4 columns (4x4)

1 2 3 4
5 6 7 8
9 10 11 12
13 14 15 16

Assign a Boolean variable to each cell of the board as below (1, 2, 3, etc. are variable names) If a variable is True, then there is a queen on the corresponding cell and vice versa. Use CNF clauses to describe constraints to place a queen on cell no. 1

use -1 to denote NOT 1

The table below is my CNF answer. I wonder if I did the right thing?. Can you check it for me?. Thanks

No CNF
1 9 ^ -5 ^ -1 ^ -13 ^ -10 ^ -11 ^ -12 ^ -6 ^ -3 ^ -14
2 2 ^ -1 ^ -3 ^ -4 ^ -6 ^ -10 ^ -14 ^ -5 ^ -7 ^ -12
3 15 ^ -13 ^ -14 ^ -16 ^ -11 ^ -7 ^ -3 ^ -12 ^ -10 ^ -5
4 8 ^ -7 ^ -6 ^ -5 ^ -4 ^ -12 ^ -16 ^ -11 ^ -14 ^ -3
• We discourage "please check whether my answer is correct" questions, as only "yes/no" answers are possible, which won't help you or future visitors. See here and here. Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher.
– D.W.
Jul 27, 2021 at 16:14

No, your answer is not correct, and for some reason you have four CNFs (I didn't understand why).

I'll give you some hints, how to reduce the Four Queens Problem to a CNF. I'll use notation, which is common for boolean variables and expressions. A boolean variable $$x_{i,j}$$, where $$i,j \in [1,4]$$, will be used to represent a queen in the cell $$(i,j)$$.

1. You need to express the first requirement, that each row and each column contains at least one queen, as a boolean expression. This can be done with the aid of the logical OR operation ($$\lor$$). You need to logically OR all the $$x_{i,j}$$ variables separately for each row and each column. For example, this requirement for the first row can be expressed as:

$$x_{1,1} \lor x_{1,2} \lor x_{1,3} \lor x_{1,4}$$

1. Also you need to express the second requirement, that all the queens don't pairwise attack each other. So, for each pair $$((i,j),(k,l))$$ of cells, such that a queen at the cell $$(i,j)$$ can attack the cell $$(k,l)$$, their corresponding variables $$x_{i,j}$$ and $$x_{k,l}$$ can't be both equal to $$true$$. The boolean expression $$(\lnot x_{i,j} \lor \lnot x_{k,l})$$ guarantees just that. For example, cells $$(1,1)$$ and $$(3,3)$$ are on the main diagonal, so the boolean expression below guarantees, that two queens can't be placed simultaneously at these two cells.

$$\lnot x_{1,1} \lor \lnot x_{3,3}$$

You can use these two types of clauses to create a CNF, which describes this problem as a CNF satisfiability problem - however, this CNF will be long (84 clauses). That's why (I think) you were asked to write a shorter CNF, which includes only clauses, where the variable $$x_{1,1}$$ is present.