Reasearch On Heuristic SMT Solver Based On Lazy Framework

With the development of science and technology, the judgment of the formula satisfaction have important application value in formal verification, artificial intelligence and many other fields, and it gradually becomes a research topic in recent years. This paper first introduces the SAT problem, and then introduces some classic SAT solvers. But the problem of SAT is only related to the proposition logic, and its expression ability is limited. However, the problem of SMT is the theory of the satisfied modules in the first order logic, which extends the expression range of the propositional logic. Then introduces the SMT problem and some classical SMT solvers framework. Then analysis of the compiling principles of the makefile and libtools tools, as a result we reconstruct the architecture of the SMT solver to generate nu SMT. At last, we combine with different algorithms respectively in this framework and form some new SMT solver GASMT,GSASMT, CCGSMT and RSSMT. We also test some instance and make analysis.This paper has made the research results as follows.(1) We reconstruct the architecture of SMT solver and generate nu SMT.(2)Apply the swarm intelligence algorithm to the resolution of SMT problem and generate a new GASMT solver and test some SMT examples.(3)We combine the original Solar, EAs and GA with theory solver,and develop a new SMT solver GSASMT. We also compare and analyze the solution effect of GSASMT and GHSMT.(4) We combine the CCGscore and Riss with theory solver respectively, and generate the new SMT solvers CCGSMT and RSSMT. Then test and analyze the some SMT Benchmarks by using CCGSMT and RSSMT respectively.