Lemma learning in SMT on linear constraints

The past decade has seen great improvement in Boolean Satisfiability(SAT) solvers. SAT solving is now widely used in different areas, including electronic design automation, software verification and artificial intelligence. However, many applications have non-Boolean constraints, such as linear relations and uninterpreted functions. Converting such constraints into SAT is very hard and sometimes impossible. This has given rise to a recent surge of interest in Satisfiability Modulo Theories (SMT). SMT incorporates predicates in other theories such as linear real arithmetic, into a Boolean formula. Solving an SMT problem entails either finding an assignment for all Boolean and theory specific variables in the formula that evaluates the formula to TRUE or proving that such an assignment does not exist. To solve such an SMT instance, a solver typically combines SAT and theory-specific solving under the Nelson-Oppen procedure framework. Fast SAT and theory-specific solvers and good integration of the two are required for efficient SMT solving. Efficient learning contributes greatly to the success of the recent SAT solvers. However, the learning technique in SMT is limited in the current literature. In this paper, we propose methods of efficient lemma learning on SMT problems with linear real/integer arithmetic constraints. We describe a static learning technique that analyzes the relationship of the linear constraints. We also discuss a conflict driven learning technique derived from infeasible sets of linear real/integer constraints. The two learning techniques can be expanded to many other theories. Our experimental results show that lemma learning can significantly improve the speed of SMT solvers.