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 条

[11] SAT Modulo Monotonic Theories
Bayless, Sam
Bayless, Noah
Hoos, Holger H.
Hu, Alan J.
PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2015, : 3702 - 3709
[12] Splitting on demand in SAT modulo theories
Barrett, Clark
Nieuwenhuis, Robert
Oliveras, Albert
Tinelli, Cesare
Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2006, 4246 : 512 - 526
[13] On SAT modulo theories and optimization problems
Nieuwenhuis, Robert
Oliveras, Albert
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 156 - 169
[14] A new FPGA-based DPLL algorithm to improve SAT solvers
Bousmar, Khadija
Monteiro, Fabrice
Habbas, Zineb
Dellagi, Sofiene
Dandache, Abbas
2015 27TH INTERNATIONAL CONFERENCE ON MICROELECTRONICS (ICM), 2015, : 287 - 290
[15] A DPLL-based calculus for ground satisfiability modulo theories
Tinelli, C
LOGICS IN ARTIFICIAL INTELLIGENCE 8TH, 2002, 2424 : 308 - 319
[16] Beyond boolean SAT: Satisfiability Modulo Theories
Cimatti, Alessandro
WODES' 08: PROCEEDINGS OF THE 9TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, 2008, : 68 - 73
[17] A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
Baader, F
Tinelli, C
AUTOMATED DEDUCTION - CADE-14, 1997, 1249 : 19 - 33
[18] Understanding the dynamic behaviour of modern DPLL SAT solvers through visual analysis
Brien, Cameron
Malik, Sharad
PROCEEDINGS OF FORMAL METHODS IN COMPUTER AIDED DESIGN, 2006, : 49 - +
[19] Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools
Nieuwenhuis, R
Oliveras, A
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 23 - 46
[20] SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering
Nieuwenhuis, Robert
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING-CP 2010, 2010, 6308 : 1 - 2

← 1 2 3 →