【CSE 260 Pair】CSE 260
CSE 260 Spring 2021
Pair Assignment 5
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:
? There has to be at most one queen in each row:
? No column contains more than one queens:
? 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.
推荐阅读
- 算法|近似算法的近似率_选择最佳近似最近算法的数据科学家指南
- 统计学|统计方法巡礼（一）算命先生和统计方法
- STU33009 统计分析
- pytorch深度学习实战|Mask R-CNN详解（图文并茂）
- 机器学习|实例分割模型Mask R-CNN详解——从R-CNN，Fast R-CNN，Faster R-CNN再到Mask R-CNN
- 计算机视觉|基于聚类的图像分割-Python
- 深度学习|【李宏毅机器学习】Convolutiona Neural Network 卷积神经网络（p17） 学习笔记
- 机器学习|【学习笔记】李宏毅2021春机器学习课程第三节（卷积神经网络（CNN））
- 李宏毅2022ML学习笔记|李宏毅老师2022机器学习课程笔记 01 Introduction of Deep Learning