计算机科学中使用的数理逻辑2015

1西安电子科技大学研究生课程考试试题（答案必须写在答题纸上或在答题卡上填涂）考试科目：课程编号：考试日期：2016年1月22日考试时间：120分考试方式：(闭卷)任课教师：班号学生姓名：学号：1.(20分)GivethediagramderivingfromtheShannonexpansionformulaoffunction𝑓(usingBinaryDecisionDiagrams).𝑓=𝐵(𝐴̅𝐶∨𝐶̅𝐸̅)∨𝐸̅(𝐴̅𝐵∨𝐵̅𝐷)22.(20分)Transformthefollowingarbitraryfunctiongraphintoareducedgraphdenotingthesamefunction.3.(15分)JudgeifthereareconflictingclausesinthefollowingCNFs.Ifnot,writeallfeasibleassignments.不行就画个真值表。。。3(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所以说，所有的值都使得这个语句结果为0，根据定义，是冲突语句(2)(x̅∨y∨z̅)(x∨y̅∨𝑧)(x∨𝑦∨𝑧)(x̅∨y̅)(x∨y̅∨𝑧)(x∨𝑦∨𝑧)=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=1x=1,x̅∨y=y=1,y̅∨z=z=1存在x、y、z的值，使得这个语句结果不为0，所以不是冲突语句。44.(10分)Provethefollowingequation.(𝑥+𝑦)(𝑦′+𝑧)≡(𝑥+𝑦)(𝑦′+𝑧)(𝑥+𝑧)画个真值表xyzx+yy’+z左x+z右0000100000101010010100000111111110011111101111111101001011111111由真值表可知，(𝑥+𝑦)(𝑦′+𝑧)≡(𝑥+𝑦)(𝑦′+𝑧)(𝑥+𝑧)5.(15分)Translatethefollowingprogramintologicalformula.Program:5Statevariables:𝑉:(𝑥,𝑦∶𝑛𝑎𝑡𝑢𝑟𝑎𝑙𝜋1∶{𝑙0,𝑙1,𝑙2,𝑙3}𝜋2∶{𝑚0,𝑚1})Initialcondition:𝛩∶𝜋1=𝑙0∧𝜋2=𝑚0∧𝑥=𝑦=0.Transitionrelation:𝜌:𝜌𝐼∨𝜌𝑙0∨𝜌𝑙1∨𝜌𝑙2∨𝜌𝑚0Writethedisjuncts𝜌𝑙0and𝜌𝑚0.(Forexample:𝜌𝐼:𝜋1′=𝜋1∧𝜋2′=𝜋2∧𝑥′=𝑥∧𝑦′=𝑦)𝜌𝑚0:𝜋2=𝑚0∧𝜋2′=𝑚1∧𝜋1′=𝜋1∧𝑥′=1∧𝑦′=𝑦6.(20分)ClausedatastoremechanisminChaffsolver.6.1Chaffstoresclausedatainalargearray.Listtheadvantagesofusingarraycomparedwithpointerdatastructure.（5分）1.在存储器上利用非常有效2.占用连续内存空间，访问局部速度加快3.数组数据结构与链表相比，就高速缓存缺失（cachemisses）而言，有一个很大优势，它在求解过程中转化为可观的加速。6.2Designadatastructurebasedonarraystostoreclausedata.（15分）Itisinvariantthatinanystatewhereaclausecanbecomenewlyimplied,bothwatchedliteralsarenotassignedto0.Akeybenefitofthetwoliteralwatchingschemeisthatatthetimeofbacktracking,thereisnoneedtomodifythewatchedliteralsintheclausedatabase.Therefore,unassigningavariablecanbedoneinconstanttime.Further,reassigningavariablethathasbeenrecentlyassignedand6unassignedwilltendtobefasterthanthefirsttimeitwasassigned.Thisistruebecausethevariablemayonlybewatchedinasmallsubsetoftheclausesinwhichwaspreviouslywatched.Thissignificantlyreducesthetotalnumberofmemoryaccesses,which,exacerbatedbythehighdatacachemissrateisthemainbottleneckformostSATimplementations.Figure1illustratesthistechnique.Itshowshowthewatchedliteralsforasingleclausechangeunderaseriesofassignmentsandunassignments.Notethattheinitialchoiceofwatchedliteralsisarbitrary,andthatforthepurposesofthisexample,theexactdetailsofhowthesequenceofassignmentsandunassignmentsisbeinggeneratedisirrelevant.7.