Splitting on Demand in Satisfiability Modulo Theories

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=DaK55BX8Zoc


Duration: 1:24:31
238 views
5

Lazy algorithms for Satisfiability Modulo Theories (SMT) combine a generic DPLL-based SAT engine with a theory solver for a given theory T that can decide the T-consistency of conjunctions of ground literals. For many theories of interest, theory solvers need to reason by performing internal case splits. In this talk we argue that it is more convenient to delegate these case splits to the DPLL engine instead. The delegation can be done on demand for solvers that can encode their internal case splits into one or more clauses, possibly including new constants and literals. This results in drastically simpler theory solvers. We present this splitting-on-demand idea in an extension of Abstract DPLL Modulo Theories, a framework for modeling and reasoning about lazy algorithms for SMT. We also show that splitting-on-demand can be naturally refined to include efficient Nelson-Oppen-like combination of multiple theories and their solvers.



Other Videos By Microsoft Research


2016-09-07Lattice-Based Discriminative Training: Theory and Practice
2016-09-07Conference XP - Tutored Video Instruction With Conference XP and Classroom Presenter
2016-09-07Faster Decoding with Synchronous Grammars and n-gram Language Models
2016-09-07Locality and Phases: Dynamic Structures in Large-Scale Program Behavior
2016-09-07Inversion Transduction Grammar with Linguistic Constraints
2016-09-07How scheduling theory, scenarios, model checking and slicing can help in the verification of RTS
2016-09-07Innovention - the process of innovation and invention
2016-09-07Security and Privacy in Radio Frequency Identification
2016-09-07Conference XP - Automated Tracking of Student Behaviors
2016-09-07From Models to Systems: Applications of Model-based Design to Modern Large-Scale Systems
2016-09-07Splitting on Demand in Satisfiability Modulo Theories
2016-09-07Making Semiconductors Ferromagnetic: Reasons, Challenges, and Opportunities
2016-09-07Exploiting comparable corpora
2016-09-07Invisible Engines: How Software Platforms Drive Innovation        
2016-09-07Towards Documenting and Automating Collateral Evolutions in Linux Device Driver
2016-09-07Phonological Licensing of Grammatical Morphology in Early Speech
2016-09-07Purpose: The Starting Point of Great Companies          
2016-09-07Location, Time and Context in Systems: Rover - An Example
2016-09-07Exploring Tools and Techniques for Distributed Continuous Quality Assurance
2016-09-07QuickSilver Scalable Multicast
2016-09-07Splitting Interfaces: Making Trust Between Applications and Operating Systems Configurable


Tags:
microsoft research