合肥生活安徽新聞合肥交通合肥房產生活服務合肥教育合肥招聘合肥旅游文化藝術合肥美食合肥地圖合肥社保合肥醫院企業服務合肥法律

        代做CMPT 477、代寫Java/python語言編程
        代做CMPT 477、代寫Java/python語言編程

        時間:2024-10-02  來源:合肥網hfw.cc  作者:hfw.cc 我要糾錯



        CMPT **7 / 777 Formal Verification
        Programming Assignment 1
        This assignment is due by 11:59pm PT on Wednesday Oct 2, 2024. Please submit it to Canvas. Late policy:
        Suppose you can get n (out of 100) points based on your code and report
        • If you submit before the deadline, you can get all n points.
        • If you submit between 11:59pm PT Oct 2 and 11:59pm PT Oct 3, you get n − 10 points. • If you submit between 11:59pm PT Oct 3 and 11:59pm PT Oct 4, you get n − 20 points. • If you submit after 11:59pm PT Oct 4, you get 0 points.
        Problem Description
        (100 points) A solution to a graph coloring problem is an assignment of colors to vertices such that no two adjacent vertices have the same color. Formally, a finite graph G = (V,E) consists of vertices V = {v1,...,vn} and edges E = {(vi1,wi1),...,(vik,wik)}. The finite set of colors is given by C = {c1,...,cm}. A problem instance is given by a graph and a set of colors: the problem is to assign each vertex v ∈ V a color(v) ∈ C such that for every edge (v,w) ∈ E, color(v) ̸= color(w). Clearly, not all instances have solutions.
        Please write a Java program with Z3 APIs to solve the graph coloring problem. The input is a file in the following format
        NM
        vi1 wi1
        vi2 wi2
        ...
        vik wik
        where the first line contains two positive integers: N is the number of vertices, and M is the number of colors (separated by a space). Without loss of generality, we can assume V = {1,...,N} and C = {1,...,M}. Each of the rest line contains two positive integers vij and wij that are no more than N, which corresponds to an edge (vij , wij ).
        The output is also a file. If an instance does not have a solution, write “No Solution” in the output file. Otherwise, write an assignment of colors to vertices in the following format.
        v1 c1
        v2 c2
        ...
        vm ck
        where vi denotes the vertex and ci denotes its color, i.e., color(vi) = ci, separated by a space.
        You might want to use the following hints for encoding: • Introduce a boolean variable pv,c for color(v) = c.
        • Describe the formula asserting every vertex is colored.
        1

        • Describe the formula asserting every vertex has at most one color.
        • Describe the formula asserting that no two connected vertices have the same color.
        2 Sample Input and Output
        Suppose we have an input file input.txt that contains the following six lines
        which represents the following graph
        43 12 13 14 24 34
        12
        34
           After running the program, we can get a file with the following lines (not unique)
        11 22 ** 43
        It means the colors of vertices v1, v2, v3, v4 are c1, c2, c2, c3, respectively. 3 Compilation and Execution
        Compilation. The provided codebase uses the Maven build system. After you enter the verif-sat direc- tory, the project can be easily compiled with one command
        $ mvn package
        Then you should be able to see the message “BUILD SUCCESS”. A directory called target will be created
        and a jar file called verif-sat-1.0.jar will be generated inside the target.
        Execution. In the verif-sat directory, you can execute the program using the following command (use ;
        instead of : on Windows)
        $ java -cp lib/com.microsoft.z3.jar:target/verif-sat-1.0.jar sat.GraphColoring <in-path> <out-path>
        where <in-path> is the path to the input file and <out-path> is the path to the output file. For example, you can run
        $ java -cp lib/com.microsoft.z3.jar:target/verif-sat-1.0.jar sat.GraphColoring input.txt output.txt
        You will see a runtime exception with message “To be implemented”, because the program is not imple- mented yet. After you finish the implementation, you should see a file named output.txt with the content as shown in Section 2.
        2

        4 Deliverable
        A zip file called P1 SFUID.zip (SFUID is replaced with your 9-digit student ID number) that contains the followings:
        • The verif-sat directory that contains your Java program. You can have multiple source files if you want, but you need to make sure the project can be built and executed in the way described in Section 3.
        • A short report called P1 SFUID.pdf that describes your encoding and explains the design choices, features, issues (if any), and anything else that you want to explain about your program.
        3

        請加QQ:99515681  郵箱:99515681@qq.com   WX:codinghelp






         

        掃一掃在手機打開當前頁
      1. 上一篇:CVEN9612代寫、代做Java/Python程序設計
      2. 下一篇:代做COMP3230、代寫c/c++編程設計
      3. 無相關信息
        合肥生活資訊

        合肥圖文信息
        急尋熱仿真分析?代做熱仿真服務+熱設計優化
        急尋熱仿真分析?代做熱仿真服務+熱設計優化
        出評 開團工具
        出評 開團工具
        挖掘機濾芯提升發動機性能
        挖掘機濾芯提升發動機性能
        海信羅馬假日洗衣機亮相AWE  復古美學與現代科技完美結合
        海信羅馬假日洗衣機亮相AWE 復古美學與現代
        合肥機場巴士4號線
        合肥機場巴士4號線
        合肥機場巴士3號線
        合肥機場巴士3號線
        合肥機場巴士2號線
        合肥機場巴士2號線
        合肥機場巴士1號線
        合肥機場巴士1號線
      4. 短信驗證碼 酒店vi設計 NBA直播 幣安下載

        關于我們 | 打賞支持 | 廣告服務 | 聯系我們 | 網站地圖 | 免責聲明 | 幫助中心 | 友情鏈接 |

        Copyright © 2025 hfw.cc Inc. All Rights Reserved. 合肥網 版權所有
        ICP備06013414號-3 公安備 42010502001045

        主站蜘蛛池模板: 国产微拍精品一区二区| 无码毛片一区二区三区视频免费播放 | 国产精品亚洲不卡一区二区三区| 精品一区二区久久久久久久网站| 精彩视频一区二区| 亚洲av午夜福利精品一区| 在线精品一区二区三区电影| 91精品福利一区二区三区野战| 亚洲av午夜精品一区二区三区| 亚洲丶国产丶欧美一区二区三区 | 国产AⅤ精品一区二区三区久久| 中文字幕精品一区二区| 日韩爆乳一区二区无码| 无码人妻精品一区二区三| 人妻少妇一区二区三区| 国产一区二区高清在线播放| 一区二区三区美女视频| 午夜精品一区二区三区在线视 | 亚洲一区二区三区国产精品| 国内精自品线一区91| 国精产品一区一区三区有限在线| 亚洲av无码一区二区三区天堂古代| a级午夜毛片免费一区二区| 久久99国产一区二区三区| 三上悠亚亚洲一区高清| 国产一区二区三区在线视頻| 自慰无码一区二区三区| 人妻少妇AV无码一区二区| 精品一区二区三区免费 | 99无码人妻一区二区三区免费| 91视频一区二区| 日本高清一区二区三区| 日韩AV片无码一区二区不卡| 无码8090精品久久一区| 国模吧无码一区二区三区| 久久婷婷久久一区二区三区| 亚洲av无码一区二区三区观看| 国产一区二区好的精华液| 精品一区二区三区无码免费直播| 亚洲av成人一区二区三区在线观看 | 免费av一区二区三区|