Representation of 3-queens problem as boolean expression for SAT solver
up vote
0
down vote
favorite
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.
logic boolean-algebra
asked Nov 16 at 20:14
Ben French
547
add a comment |
up vote
0
down vote
favorite
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.
logic boolean-algebra
asked Nov 16 at 20:14
Ben French
547
You meant (a∨b∨c) ∧ ~( a∧b) ∧ ~( a∧c) ∧ ~( b∧c). For the $n$-queens you might want to implement $n mapsto n+a_i$ in SAT, so you can define the rule $sum_i a_i = 1$
– reuns
Nov 16 at 20:18
yeah that makes sense, thanks!
– Ben French
Nov 16 at 20:23
add a comment |
up vote
0
down vote
favorite
up vote
0
down vote
favorite
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.
logic boolean-algebra
asked Nov 16 at 20:14
Ben French
547
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.
logic boolean-algebra
logic boolean-algebra
asked Nov 16 at 20:14
Ben French
547
asked Nov 16 at 20:14
Ben French
547
asked Nov 16 at 20:14
Ben French
547
asked Nov 16 at 20:14
Ben French
547
asked Nov 16 at 20:14
Ben French
547
547
You meant (a∨b∨c) ∧ ~( a∧b) ∧ ~( a∧c) ∧ ~( b∧c). For the $n$-queens you might want to implement $n mapsto n+a_i$ in SAT, so you can define the rule $sum_i a_i = 1$
– reuns
Nov 16 at 20:18
yeah that makes sense, thanks!
– Ben French
Nov 16 at 20:23
add a comment |
You meant (a∨b∨c) ∧ ~( a∧b) ∧ ~( a∧c) ∧ ~( b∧c). For the $n$-queens you might want to implement $n mapsto n+a_i$ in SAT, so you can define the rule $sum_i a_i = 1$
– reuns
Nov 16 at 20:18
yeah that makes sense, thanks!
– Ben French
Nov 16 at 20:23
You meant (a∨b∨c) ∧ ~( a∧b) ∧ ~( a∧c) ∧ ~( b∧c). For the $n$-queens you might want to implement $n mapsto n+a_i$ in SAT, so you can define the rule $sum_i a_i = 1$
– reuns
Nov 16 at 20:18
You meant (a∨b∨c) ∧ ~( a∧b) ∧ ~( a∧c) ∧ ~( b∧c). For the $n$-queens you might want to implement $n mapsto n+a_i$ in SAT, so you can define the rule $sum_i a_i = 1$
– reuns
Nov 16 at 20:18
yeah that makes sense, thanks!
– Ben French
Nov 16 at 20:23
yeah that makes sense, thanks!
– Ben French
Nov 16 at 20:23
add a comment |
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
Exactly one queen on top row : (a∨b∨c) ∧ ~( a∧b∧c)
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 ...
answered Nov 16 at 20:18
Bram28
58.5k44185
add a comment |
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
Exactly one queen on top row : (a∨b∨c) ∧ ~( a∧b∧c)
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 ...
answered Nov 16 at 20:18
Bram28
58.5k44185
add a comment |
up vote
1
down vote
accepted
Exactly one queen on top row : (a∨b∨c) ∧ ~( a∧b∧c)
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 ...
answered Nov 16 at 20:18
Bram28
58.5k44185
add a comment |
up vote
1
down vote
accepted
up vote
1
down vote
accepted
Exactly one queen on top row : (a∨b∨c) ∧ ~( a∧b∧c)
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 ...
answered Nov 16 at 20:18
Bram28
58.5k44185
Exactly one queen on top row : (a∨b∨c) ∧ ~( a∧b∧c)
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 ...
answered Nov 16 at 20:18
Bram28
58.5k44185
answered Nov 16 at 20:18
Bram28
58.5k44185
answered Nov 16 at 20:18
Bram28
58.5k44185
answered Nov 16 at 20:18
Bram28
58.5k44185
58.5k44185
add a comment |
add a comment |
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3001596%2frepresentation-of-3-queens-problem-as-boolean-expression-for-sat-solver%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
You meant (a∨b∨c) ∧ ~( a∧b) ∧ ~( a∧c) ∧ ~( b∧c). For the $n$-queens you might want to implement $n mapsto n+a_i$ in SAT, so you can define the rule $sum_i a_i = 1$
– reuns
Nov 16 at 20:18
yeah that makes sense, thanks!
– Ben French
Nov 16 at 20:23