资源描述：
《计算机科学中使用的数理逻辑2015.docx》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、西安电子科技大学研究生课程考试试题（答案必须写在答题纸上或在答题卡上填涂）考试科目：课程编号：考试日期：2016年1月22日考试时间：120分考试方式：(闭卷)任课教师：班号学生姓名：学号：1.(20分)GivethediagramderivingfromtheShannonexpansionformulaoffunctionf(usingBinaryDecisionDiagrams).f=B(AC∨CE)∨E(AB∨BD)1.(20分)Transformthefollowingarbitraryfunctiongraphintoar
2、educedgraphdenotingthesamefunction.2.(15分)JudgeifthereareconflictingclausesinthefollowingCNFs.Ifnot,writeallfeasibleassignments.不行就画个真值表。。。(1)(x∨y∨z)(x∨y)(y∨z)(z∨x)(x∨y∨z)假设x=0,(x∨y)=>y=0+(y∨z)=>z=0x=0,y=0,z=0=>(x∨y∨z)=0假设x=1,(z∨x)=>z=1+(y∨z)=>y=1x=1,y=1,z=1,(x∨y∨z)=>0所
3、以说，所有的值都使得这个语句结果为0，根据定义，是冲突语句(2)(x∨y∨z)(x∨y∨z)(x∨y∨z)(x∨y)(x∨y∨z)(x∨y∨z)=>x∨z(x∨y)(x∨y∨z)=>(x∨z)所以，x、z一个为1a.x=1,z=0,x∨y=>y=0b.x=0,z=1,y随便存在x、y、z的值，使得这个语句结果不为0，所以不是冲突语句。(3)(x∨y∨z)(y∨z)(x∨y)(y∨z)(x∨y∨z)(y∨z)(x∨y∨z)=>y∨z(x∨y∨z)(x∨y∨z)=>x∨y(y∨z)(x∨y)=>x∨zx=0,x∨z,x∨y=>z=1,y=
4、1x=1,x∨y=>y=1,y∨z=>z=1存在x、y、z的值，使得这个语句结果不为0，所以不是冲突语句。1.(10分)Provethefollowingequation.(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)2.(15分)Translatethefollowingprogramin
5、tologicalformula.Program:Statevariables:V:x,y:naturalπ1:{l0,l1,l2,l3}π2:m0,m1Initialcondition:Θ:π1=l0∧π2=m0∧x=y=0.Transitionrelation:ρ:ρI∨ρl0∨ρl1∨ρl2∨ρm0Writethedisjunctsρl0andρm0.(Forexample:ρI:π1'=π1∧π2'=π2∧x'=x∧y'=y)ρm0:π2=m0∧π2'=m1∧π1'=π1∧x'=1∧y'=y1.(20分)Clausedatas
6、toremechanisminChaffsolver.1.1Chaffstoresclausedatainalargearray.Listtheadvantagesofusingarraycomparedwithpointerdatastructure.（5分）1.在存储器上利用非常有效2.占用连续内存空间，访问局部速度加快3.数组数据结构与链表相比，就高速缓存缺失（cachemisses）而言，有一个很大优势，它在求解过程中转化为可观的加速。1.2Designadatastructurebasedonarraystostorecla
7、usedata.（15分）Itisinvariantthatinanystatewhereaclausecanbecomenewlyimplied,bothwatchedliteralsarenotassignedto0.Akeybenefitofthetwoliteralwatchingschemeisthatatthetimeofbacktracking,thereisnoneedtomodifythewatchedliteralsintheclausedatabase.Therefore,unassigningavariable
8、canbedoneinconstanttime.Further,reassigningavariablethathasbeenrecentlyassignedandunassignedwilltendtobefaster
