Challenges in satisfiability modulo theories

被引:0
|
作者
Nieuwenhuis, Robert [1 ]
Oliveras, Albert [1 ]
Rodriguez-Carbonell, Enric [1 ]
Rubio, Albert [1 ]
机构
[1] Tech Univ Catalonia, Barcelona, Spain
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Here we give a short overview of the DPLL(T) approach to Satisfiability Modulo Theories (SMT), which is at the basis of current state-of-the-art SMT systems. After that, we provide a documented list of theoretical and practical current challenges related to SMT, including some new ideas to exploit SAT techniques in Constraint Programming.
引用
收藏
页码:2 / +
页数:3
相关论文
共 50 条
  • [1] Satisfiability modulo theories
    Barrett, Clark
    Sebastiani, Roberto
    Seshia, Sanjit A.
    Tinelli, Cesare
    [J]. Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) : 825 - 885
  • [2] From propositional satisfiability to satisfiability modulo theories
    Sheini, Hossein M.
    Sakallah, Karem A.
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 1 - 9
  • [3] A framework for Satisfiability Modulo Theories
    Kroening, Daniel
    Strichman, Ofer
    [J]. FORMAL ASPECTS OF COMPUTING, 2009, 21 (05) : 485 - 494
  • [4] Satisfiability Modulo Theories: An Appetizer
    de Moura, Leonardo
    Bjorner, Nikolaj
    [J]. FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, 2009, 5902 : 23 - 36
  • [5] Satisfiability Modulo Theories and Assignments
    Bonacina, Maria Paola
    Graham-Lengrand, Stephane
    Shankar, Natarajan
    [J]. AUTOMATED DEDUCTION - CADE 26, 2017, 10395 : 42 - 59
  • [6] Foundations of Satisfiability Modulo Theories
    Tinelli, Cesare
    [J]. LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, 2010, 6188 : 58 - 58
  • [7] An abstract framework for satisfiability modulo theories
    Tinelli, Cesare
    [J]. Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings, 2007, 4548 : 10 - 10
  • [8] Combined satisfiability modulo parametric theories
    Krstic, Sava
    Goel, Amit
    Grundy, Jim
    Tinelli, Cesare
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 602 - +
  • [9] An Instantiation Scheme for Satisfiability Modulo Theories
    Echenim, Mnacho
    Peltier, Nicolas
    [J]. JOURNAL OF AUTOMATED REASONING, 2012, 48 (03) : 293 - 362
  • [10] Motion Planning with Satisfiability Modulo Theories
    Hung, William N. N.
    Song, Xiaoyu
    Tan, Jindong
    Li, Xiaojuan
    Zhang, Jie
    Wang, Rui
    Gao, Peng
    [J]. 2014 IEEE INTERNATIONAL CONFERENCE ON ROBOTICS AND AUTOMATION (ICRA), 2014, : 113 - 118