Paper Info
Title
Lemma learning in SMT on linear constraints
Abstract
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.
Year
DOI
Venue
2006
10.1007/11814948_17
SAT
Keywords
Field
DocType
lemma learning,linear constraint,efficient smt,smt instance,smt solvers,learning technique,smt problem,static learning technique,recent sat solvers,fast sat,efficient learning,electronic design automation,artificial intelligent,software verification,sat solver,satisfiability modulo theories,boolean satisfiability
Discrete mathematics,Constraint satisfaction,Computer science,Boolean satisfiability problem,Satisfiability,Propositional calculus,Theoretical computer science,Boolean algebra,True quantified Boolean formula,Lemma (mathematics),Satisfiability modulo theories
Conference
Volume
ISSN
ISBN
4121
0302-9743
3-540-37206-7
Citations 
PageRank 
References 
7
0.58
17
Authors
2
Name
Order
Citations
PageRank
Yinlei Yu1955.96
Sharad Malik27766691.24