The Enhancement Techniques To SMT Solvers

In the age of remarkable development of IC technology, the complexity of both hardware and software designs are increasing rapidly. In addition, there are some new challenges for designing and developing new products, especially for guaranteeing security, reliability and soundness for specific requirements. To solve the new problems, computer aided verification and testing tools are exploited. Both Satisfiability(SAT) and Satisfiability Modulo Theories(SMT) have become hotspots in the last decade. With the improvements to relevant techniques, SAT/SMT tools have found many applications in various regions. In this thesis, a SMT solver is improved and applied in optimization problems, which is a region a SMT may play important roles.Concretely, we have made the following efforts to enhance both the performance and the functionality of a SMT solver:1. Based on the study of current conflict analysis techniques, a new method is proposed. The goal of our approach is to decrease the number of conflicts during the search process and fully utilize these conflict nodes to generate more effective and more concise conflict clauses. Although our approach may increase the number of additional clauses to the clause library, with these more informational clauses, the solver can avoid more conflict in the future and thus runs faster.2. We have studied and improved CNF preprocessing techniques. The preprocessing will simplify CNF formula before starting the solving process. One feature of a modern SAT solver is their performance depends on the way the relations between variables are expressed. For example, a CNF formula with more asserting clauses, a clause with less literals, will be more helpful for solving the problem sooner. This is the main source of ideas we propose to handle the problem.3. We extend a SMT solver for optimization applications. We propose a novel method to tune a SMT solver for solving optimization problems. Our inspiration comes from the necessary conditions for extrema of multivariable functions. In our work, such necessary conditions are added to the clause library of the Boolean abstraction of the SMT problem. All extrema are enumerated through the DPLL procedure among which the optimal one can be acquired. The feasibility of the method is demonstrated by experiments. Based on SATEEn, a SMT solver developed by VLSI/CAD Research Group in University of Colorado at Boulder, we implement our method with C and lex&yacc, and conduct some experiments to prove soundness and feasibility of our approach.