首页
网站开发
桌面应用
管理软件
微信开发
App开发
嵌入式软件
工具软件
数据采集与分析
其他
首页
>
> 详细
讲解CSE 260程序、辅导Python,Java程序、c++编程调试 辅导R语言程序|讲解R语言编程
项目预算:
开发周期:
发布时间:
要求地区:
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
软件开发、广告设计客服
QQ:99515681
邮箱:99515681@qq.com
工作时间:8:00-23:00
微信:codinghelp
热点项目
更多
代做ceng0013 design of a pro...
2024-11-13
代做mech4880 refrigeration a...
2024-11-13
代做mcd1350: media studies a...
2024-11-13
代写fint b338f (autumn 2024)...
2024-11-13
代做engd3000 design of tunab...
2024-11-13
代做n1611 financial economet...
2024-11-13
代做econ 2331: economic and ...
2024-11-13
代做cs770/870 assignment 8代...
2024-11-13
代写amath 481/581 autumn qua...
2024-11-13
代做ccc8013 the process of s...
2024-11-13
代写csit040 – modern comput...
2024-11-13
代写econ 2070: introduc2on t...
2024-11-13
代写cct260, project 2 person...
2024-11-13
热点标签
mktg2509
csci 2600
38170
lng302
csse3010
phas3226
77938
arch1162
engn4536/engn6536
acx5903
comp151101
phl245
cse12
comp9312
stat3016/6016
phas0038
comp2140
6qqmb312
xjco3011
rest0005
ematm0051
5qqmn219
lubs5062m
eee8155
cege0100
eap033
artd1109
mat246
etc3430
ecmm462
mis102
inft6800
ddes9903
comp6521
comp9517
comp3331/9331
comp4337
comp6008
comp9414
bu.231.790.81
man00150m
csb352h
math1041
eengm4100
isys1002
08
6057cem
mktg3504
mthm036
mtrx1701
mth3241
eeee3086
cmp-7038b
cmp-7000a
ints4010
econ2151
infs5710
fins5516
fin3309
fins5510
gsoe9340
math2007
math2036
soee5010
mark3088
infs3605
elec9714
comp2271
ma214
comp2211
infs3604
600426
sit254
acct3091
bbt405
msin0116
com107/com113
mark5826
sit120
comp9021
eco2101
eeen40700
cs253
ece3114
ecmm447
chns3000
math377
itd102
comp9444
comp(2041|9044)
econ0060
econ7230
mgt001371
ecs-323
cs6250
mgdi60012
mdia2012
comm221001
comm5000
ma1008
engl642
econ241
com333
math367
mis201
nbs-7041x
meek16104
econ2003
comm1190
mbas902
comp-1027
dpst1091
comp7315
eppd1033
m06
ee3025
msci231
bb113/bbs1063
fc709
comp3425
comp9417
econ42915
cb9101
math1102e
chme0017
fc307
mkt60104
5522usst
litr1-uc6201.200
ee1102
cosc2803
math39512
omp9727
int2067/int5051
bsb151
mgt253
fc021
babs2202
mis2002s
phya21
18-213
cege0012
mdia1002
math38032
mech5125
07
cisc102
mgx3110
cs240
11175
fin3020s
eco3420
ictten622
comp9727
cpt111
de114102d
mgm320h5s
bafi1019
math21112
efim20036
mn-3503
fins5568
110.807
bcpm000028
info6030
bma0092
bcpm0054
math20212
ce335
cs365
cenv6141
ftec5580
math2010
ec3450
comm1170
ecmt1010
csci-ua.0480-003
econ12-200
ib3960
ectb60h3f
cs247—assignment
tk3163
ics3u
ib3j80
comp20008
comp9334
eppd1063
acct2343
cct109
isys1055/3412
math350-real
math2014
eec180
stat141b
econ2101
msinm014/msing014/msing014b
fit2004
comp643
bu1002
cm2030
联系我们
- QQ: 9951568
© 2021
www.rj363.com
软件定制开发网!