Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL

被引：0
|
作者：
Krstic, Sava [1 ]
Goel, Amit [1 ]
机构：
[1] Intel Corp, Strateg CAD Labs, Santa Clara, CA 95051 USA
来源：
FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS | 2007年 / 4720卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We offer a transition system representing a high-level but detailed architecture for SMT solvers that combine a propositional SAT engine with solvers for multiple disjoint theories. The system captures succintly and accurately all the major aspects of the solver's global operation: boolean search with across-the-board backjumping, communication of theory-specific facts and equalities between shared variables, and cooperative conflict analysis. Provably correct and prudently underspecified, our system is a usable ground for high-quality implementations of comprehensive SMT solvers.
引用
收藏
页码：1 / +
页数：4
相关论文
共 30 条
  • [1] Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
    Roberto Bruttomesso
    Alessandro Cimatti
    Anders Franzen
    Alberto Griggio
    Roberto Sebastiani
    Annals of Mathematics and Artificial Intelligence, 2009, 55 : 63 - 99
  • [2] Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
    Bruttomesso, Roberto
    Cimatti, Alessandro
    Franzen, Anders
    Griggio, Alberto
    Sebastiani, Roberto
    ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2009, 55 (1-2) : 63 - 99
  • [3] Delayed theory combination vs. Nelson-Oppen for satistiability modulo theories: A comparative analysis
    Bruttomesso, Roberto
    Cimatti, Alessandro
    Franzen, Anders
    Griggio, Alberto
    Sebastiani, Roberto
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2006, 4246 : 527 - 541
  • [4] A new correctness proof of the Nelson-Oppen combination procedure
    Tinelli, C
    Harandi, M
    FRONTIERS OF COMBINING SYSTEMS, 1996, 3 : 103 - 119
  • [5] Abstract DPLL and abstract DPLL modulo theories
    Nieuwenhuis, R
    Oliveras, A
    Tinelli, C
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3452 : 36 - 50
  • [6] Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn
    Ranise, S
    Ringeissen, C
    Tran, DK
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2004, 2005, 3407 : 372 - 386
  • [7] An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
    Lahiri, Shuvendu K.
    Musuvathi, Madanlal
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (02) : 27 - 41
  • [8] On the Convexity of a Fragment of Pure Set Theory with Applications within a Nelson-Oppen Framework
    Cantone, Domenico
    Maugeri, Pietro
    De Domenico, Andrea
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (346): : 195 - 210
  • [9] Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures
    Bonacina, Maria Paola
    Ghilardi, Silvio
    Nicolini, Enrica
    Ranise, Silvio
    Zucchelli, Daniele
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 513 - 527
  • [10] Solving SAT and SAT modulo theories:: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)
    Nieuwenhuis, Robert
    Oliveras, Albert
    Tinelli, Cesare
    JOURNAL OF THE ACM, 2006, 53 (06) : 937 - 977
123