計算機科學中使用的數(shù)理邏輯2015

1、精選優(yōu)質(zhì)文檔-傾情為你奉上精選優(yōu)質(zhì)文檔-傾情為你奉上專心-專注-專業(yè)專心-專注-專業(yè)精選優(yōu)質(zhì)文檔-傾情為你奉上專心-專注-專業(yè)西安電子科技大學研究生課程考試試題（答案必須寫在答題紙上或在答題卡上填涂）考試科目： 課程編號： 考試日期： 2016 年 1 月 22 日 考試時間： 120 分考試方式：(閉卷) 任課教師： 班號 學生姓名： 學 號： (20分) Give the diagram deriving from the Shannon expansion formula of function f (using Binary Decision Diagrams).f=B(ACCE)E(

2、ABBD)(20分) Transform the following arbitrary function graph into a reduced graph denoting the same function. (15分) Judge if there are conflicting clauses in the following CNFs. If not, write all feasible assignments.不行就畫個真值表。 (xyz)(xy)(yz)(zx)(xyz)假設x=0, (xy)=y=0+(yz)=z=0 x=0,y=0,z=0=(xyz)=0假設x=1, (

3、zx)=z=1+(yz)=y=1x=1,y=1,z=1, (xyz)=0所以說，所有的值都使得這個語句結果為0，根據(jù)定義，是沖突語句 (xyz)(xyz)(xyz)(xy)(xyz)(xyz)= xz(xy) (xyz)= (xz)所以，x、z一個為1x=1,z=0, xy=y=0 x=0,z=1, y隨便存在x、y、z的值，使得這個語句結果不為0，所以不是沖突語句。(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的值，使得這個語句

4、結果不為0，所以不是沖突語句。 (10分) Prove 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)(15分) Translate the following program into logical formula. Program:State variables: V: x,y :natural 1 :l0,l

5、1,l2,l32 :m0,m1 Initial condition: : 1=l02=m0 x=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=y(20分) Clause data store mechanism in Chaff solver.Chaff stores clause data in a large array. List the advantages of using array compar

6、ed with pointer data structure.（5分）在存儲器上利用非常有效占用連續(xù)內(nèi)存空間，訪問局部速度加快數(shù)組數(shù)據(jù)結構與鏈表相比，就高速緩存缺失（cache misses）而言，有一個很大優(yōu)勢，它在求解過程中轉(zhuǎn)化為可觀的加速。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 assign

7、ed 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 u

8、nassigned 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 rate 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 tha