《计算机科学中使用的数理逻辑2015.docx》由会员分享，可在线阅读，更多相关《计算机科学中使用的数理逻辑2015.docx（6页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、精选优质文档-倾情为你奉上西安电子科技大学研究生课程考试试题（答案必须写在答题纸上或在答题卡上填涂）考试科目： 课程编号： 考试日期： 2016 年 1 月 22 日 考试时间： 120 分考试方式：(闭卷) 任课教师： 班号 学生姓名： 学 号： 1. (20分) Give the diagram deriving from the Shannon expansion formula of function f (using Binary Decision Diagrams).f=B(ACCE)E(ABBD)2. (20分) Transform the following arbitrary
2、 function graph into a reduced graph denoting the same function. 3. (15分) Judge if there are conflicting clauses in the following CNFs. If not, write all feasible assignments.不行就画个真值表。(1) (xyz)(xy)(yz)(zx)(xyz)假设x=0, (xy)=y=0+(yz)=z=0x=0,y=0,z=0=(xyz)=0假设x=1, (zx)=z=1+(yz)=y=1x=1,y=1,z=1, (xyz)=0所以说
3、，所有的值都使得这个语句结果为0，根据定义，是冲突语句(2) (xyz)(xyz)(xyz)(xy)(xyz)(xyz)= xz(xy) (xyz)= (xz)所以，x、z一个为1a. x=1,z=0, xy=y=0b. x=0,z=1, y随便存在x、y、z的值，使得这个语句结果不为0，所以不是冲突语句。(3) (xyz)(yz)(xy)(yz)(xyz)(yz) (xyz)= yz(xyz)(xyz)= xy(yz)(xy)= xzx=0, xz,xy=z=1,y=1x=1, xy=y=1, yz=z=1存在x、y、z的值，使得这个语句结果不为0，所以不是冲突语句。4. (10分) Pro
4、ve the following equation.(x+y)(y+z)(x+y)(y+z)(x+z)画个真值表xyzx+yy+z左x+z右0000100000101010010100000111111110011111101111111101001011111111由真值表可知， (x+y)(y+z)(x+y)(y+z)(x+z)5. (15分) Translate the following program into logical formula. Program:State variables: V: x,y :natural 1 :l0,l1,l2,l32 :m0,m1 Initia
5、l condition: : 1=l02=m0x=y=0. Transition relation: :Il0l1l2m0Write the disjuncts l0 and m0.(For example: I: 1=12=2x=xy=y)m0: 2=m02=m1 1=1x=1y=y6. (20分) Clause data store mechanism in Chaff solver.6.1 Chaff stores clause data in a large array. List the advantages of using array compared with pointer
6、data structure.（5分）1. 在存储器上利用非常有效2. 占用连续内存空间，访问局部速度加快3. 数组数据结构与链表相比，就高速缓存缺失（cache misses）而言，有一个很大优势，它在求解过程中转化为可观的加速。6.2 Design a data structure based on arrays to store clause data.（15分）It is invariant that in any state where a clause can become newly implied, both watched literals are not assigned
7、to 0. A key benefit of the two literal watching scheme is that at the time of backtracking, there is no need to modify the watched literals in the clause database. Therefore, unassigning a variable can be done in constant time. Further, reassigning a variable that has been recently assigned and unas
8、signed will tend to be faster than the first time it was assigned. This is true because the variable may only be watched in a small subset of the clauses in which was previously watched. This significantly reduces the total number of memory accesses, which, exacerbated by the high data cache miss ra
9、te is the main bottleneck for most SAT implementations. Figure 1 illustrates this technique. It shows how the watched literals for a single clause change under a series of assignments and unassignments. Note that the initial choice of watched literals is arbitrary, and that for the purposes of this example, the exact details of how the sequence of assignments and unassignments is being generated is irrelevant.7.专心-专注-专业