Lemma learning in SMT on linear constraints

Yinlei Yu, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings
PublisherSpringer Verlag
Pages142-155
Number of pages14
ISBN (Print)3540372067, 9783540372066
DOIs
StatePublished - Jan 1 2006
Event9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006 - Seattle, WA, United States
Duration: Aug 12 2006Aug 15 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4121 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006
CountryUnited States
CitySeattle, WA
Period8/12/068/15/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Lemma learning in SMT on linear constraints'. Together they form a unique fingerprint.

  • Cite this

    Yu, Y., & Malik, S. (2006). Lemma learning in SMT on linear constraints. In Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings (pp. 142-155). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4121 LNCS). Springer Verlag. https://doi.org/10.1007/11814948_17