共计 1975 个字符，预计需要花费 5 分钟才能阅读完成。
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.
