Splitting on Demand in SAT Modulo Theories

DOI10.1007/11916277_35MaRDI QIDQ5387916zbMATH OpenOpenAlexFDO

Authors Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11916277_35

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Lazy satisfiability modulo theories
• An Abstract Framework for Satisfiability Modulo Theories
• Satisfiability modulo theories
• Computer Aided Verification
• An abstract interpretation of DPLL(T)

Cited in

(35)

• A framework for satisfiability modulo theories
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Solving quantified verification conditions using satisfiability modulo theories
• Theory decision by decomposition
• A decision procedure for string to code point conversion
• Reasoning about vectors using an SMT theory of sequences
• Conflict-driven satisfiability for theory combination: transition system and completeness
• SPASS-SATT. A CDCL(LA) solver
• A complete and terminating approach to linear integer solving
• Being careful about theory combination
• Colors Make Theories Hard
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• On abstract modular inference systems and solvers
• An abstract decision procedure for satisfiability in the theory of recursive data types
• Sharing is caring: combination of theories
• Satisfiability modulo theories
• Linear integer arithmetic revisited
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Combining decision procedures by (model-)equality propagation
• Constraint solving for finite model finding in SMT solvers
• Resolution proof transformation for compression and interpolation
• Deciding floating-point logic with abstract conflict driven clause learning
• Branch and bound for piecewise linear neural network verification
• Combining Decision Procedures by (Model-)Equality Propagation
• An efficient SMT solver for string constraints
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Reasoning about vectors: satisfiability modulo a theory of sequences
• Reluplex: a calculus for reasoning about deep neural networks
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• SAT Modulo Differential Equation Simulations
• The CDSAT method for satisfiability modulo theories and assignment: an exposition
• FMplex: a novel method for solving linear real arithmetic problems
• FMplex: exploring a bridge between Fourier-Motzkin and simplex
• A formal model to prove instantiation termination for E-matching-based axiomatisations

This page was built for publication: Splitting on Demand in SAT Modulo Theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5387916)