基于ST方法的命题公式不可满足性的判定系统-计算机应用技术专业论文.docxVIP

A A Checking System of Unsatisfiability based on ST Algorithm For Propositional Formulas Abstract SAT of 10sic formulas is famous problem of theoretic computer science and artificial intelligence．Checking method of satisfiabllity for propositional logic formulas and finite model constructed technology for first-order logic can be sppUed in Some fields，such discrete mathemafi∞research，the computer aided design of electronic circuits，software engineering and artificial intelligence． Many algorithms applicable for tautology checking,such Tableau Proof System、 WangHao Algorithm and Binary Decision Dlagram(BVDs)．BDD and their variations work well for other applications，SUch as model choking． StaImareks method of tautology checking may well rival BDDs[18】in some applications， but that iS relatively unlmdwn in the hardware verification community[101．nds patented method is implemented in coll]nlerciai tool that has been used in many indm仃ial svstem verification projects[1]．Often．the verification problem be expressed∞an inductive proof,and the base case and the step checked using StaImarck’s method．Many of these real-world verifications give rise to印ormous formulas that could not be handled by a肛r锄t BDD packages．Crreote has found Stalmarcks method to be very efficient compa托d to BDD-based methods and the Otter Do∞，el in the verification ofthe safety guaranteeing system at particular Dutch mflway station[12]． However,St墨Imarcks method is not perfect．Many industrial verification problems give rise to fonnulas whose haIdness is 0 w 1，for the formulas whose hardness is 0，ODe find proof in linear time without the dilemma role，but for the formulas whose hardness is 1。one must m the dilemma rule．It is not considering the case that the intersection of R1 and R2 is empty in the 、、branch and merge rule”，but it is possible that the exists．In article，we gave an example with that case and made system containing the case．Our method have improved the、、dilemma rule“，and gave perfect prov