CSE 260 Spring 2021

In this assignment, you are to solve the n-Queens problem by reducing the

problem to the propositional satisfiability problem. Recall that a propositional

formula ? is satisfiable if there is an assignment of truth values to propositional

variables in ? that makes ? true.

1 Description

The n-queens problem asks for placement of n queens on an n×n chessboard so

that no queen can attack another queen. One can encode the n-Queens problem

as a satisfiability problem as follows (more details can be found in your textbook

and on lecture slides):

? We introduce n

2 propositions. Let them be p(i, j) for i = 1, 2, . . . , n and

j = 1, 2, . . . , n, which indicates whether there is a queen in row i and

column j.

? There has to be at least one queen in each row:

? No column contains more than one queens:

? Putting all these together:

Q = Q1 ∧ Q2 ∧ Q3 ∧ Q4 ∧ Q5

? Thus, if Q is satisfiable, then the n-queens problem has a solution given

by p(i, j) for i = 1, 2, . . . , n and j = 1, 2, . . . , n.

2 Assignment

You are to solve the problem for n = 3 and n = 4 using the SMT-solver Z3.

Z3 is a tool with web-based support that can solve the proposition satisfiability

problem1

. The tool allows declaring propositional variables and including

propositional formulas for checking satifiability. If Z3 returns unsat, it means

the input formula is not satisfiable. Otherwise, it returns sat with “a model”,

which the truth assignments.

You will develop two Z3 files one for n = 3 and one for n = 4. If your Z3

submission has syntax error, you will not receive any credit. You will receive

partial credit if you make a meaningful attempt at the problem.

You are required to add comments to indicate formulas Q, Q1, . . . , Q5. Name

your propositional variables as pij, which represents p(i, j), as described above.

For example, p23, represents p(2, 3). In case of sat, the TAs will check if the

truth assignments to each p(i, j) is indeed a valid solution to the problem.

3 Extra Credit

You will receive 100% extra credit if you write a program in python that solves

the problem for any input value n. To this end, you will have to use the Z3 API

to write a program that (1) receives n as input, (2) generates the corresponding

propositional formulas, and (3) invokes the Z3 engine to determine whether the

generated formula is satisfiable.

Deliverable

Your solutions must be submitted by 11:59pm on Friday, April 2, via D2L.

1https://rise4fun.com/z3/tutorial

2

版权所有：编程辅导网 2018 All Rights Reserved 联系方式：QQ:99515681 电子信箱：99515681@qq.com

免责声明：本站部分内容从网络整理而来，只供参考！如有版权问题可联系本站删除。