Model Checking And Boolean Satisfiability Problem

In the area of hardware model checking, the original design is abstracted as finitestate transition system(or Kripke structure), while the property to be verified is repre-sented as temporal logic language. In this way, the original design will be smoothly veri-fied through checking whether the model satisfies the property considered. One tiresomebottleneck to prohibit the methodology of model checking from applying to industrialapplication is the fact that the size of the state space is growing exponentially with theincrease of the number of the state variables. The di?culty lying behind is how to rep-resent the transition relationship or the state space of model e?ectively. To alleviateor conquer the bottleneck, researchers have proposed various important approaches, forinstances, the optimized variants of Binary Decision Diagrams (BDDs), and transformingthe verification task into solving the Boolean Satisfiability (SAT) problem, as well as thevarious abstraction refinement methods performed on the original model.Under such research backgrounds, the thesis focuses on the following key problems:how to build a compact and e?cient transition relation; how to e?ciently extract MinimalUnsatisfiable (MU) sub-formula; the problem of sensitivity to the parameter called stepnumber for the Survey Propagation (SP) algorithm. Aiming to these problems, the thesisobtained the following original ideas and contributions.1. The strategy for building transition relationship is proposed in symbolic modelchecking. It is well known that a compact and e?cient transition is critical in imagecomputation. The rule proposed for grouping the partitioned transition relationshipis based on some certain feature of the support of each transition relationship part.The merit for this algorithm in building transition relationship is two-fold. On the onehand, this method can build a more compact transition, the experiments exhibit that thereduction for the size ranges from 30% to 10%,the size is measured by the number ofthe nodes in the BDD representing the transition relationship. On the other hand, thestep in image computation is partially reduced in advance.