” 写作CSE 260程序、 辅导Python，Java程序CSE 260 Spring 2021In this assignment, you are to solve the n-Queens problem by reducing theproblem to the propositional satisfiability problem. Recall that a propositionalformula is satisfiable if there is an assignment of truth values to propositionalvariables in that makes true.1 DescriptionThe n-queens problem asks for placement of n queens on an nn chessboard sothat no queen can attack Another queen. One can encode the n-Queens problemas a satisfiability problem as follows (more details can be found in your textbookand on lecture slides): We introduce n2 propositions. Let them be p(i, j) for i = 1, 2, . . . , n andj = 1, 2, . . . , n, which indicates whether there is a queen in row i andcolumn 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 givenby p(i, j) for i = 1, 2, . . . , n and j = 1, 2, . . . , n.2 AssignmentYou 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 satisfiabilityproblem1. The tool allows Declaring propositional variables and includingpropositional formulas for checking satifiability. If Z3 returns unsat, it meansthe 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 Z3submission has syntax error, you will not receive any credit. You will receivepartial credit if you make a meaningful attempt at the problem.You are required to add Comments to indicate formulas Q, Q1, . . . , Q5. Nameyour 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 thetruth assignments to each p(i, j) is indeed a valid solution to the problem.3 Extra CreditYou will receive 100% extra credit if you write a program in python that solvesthe problem for any input value n. To this end, you will have to use the Z3 APIto write a program that (1) receives n as input, (2) generates the correspondingpropositional formulas, and (3) invokes the Z3 engine to determine whether thegenerated formula is satisfiable.DeliverableYour solutions must be Submitted by 11:59pm on Friday, April 2, via D2L.1 httpss://rise4fun.com/z3/tutorial请加QQ：99515681 或邮箱：99515681@qq.com WX：codehelp
“
添加老师微信回复‘’官网 辅导‘’获取专业老师帮助，或点击联系老师1对1在线指导。
