Splitting on Demand in SAT Modulo Theories

DOI10.1007/11916277_35zbMath1165.68480OpenAlexW2159786179MaRDI QIDQ5387916

Robert Nieuwenhuis, Cesare Tinelli, Albert Oliveras, Clark Barrett

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)

Related Items

On abstract modular inference systems and solvers, Sharing Is Caring: Combination of Theories, Satisfiability Modulo Theories, Linear Integer Arithmetic Revisited, Unnamed Item, Reasoning about vectors: satisfiability modulo a theory of sequences, Constraint solving for finite model finding in SMT solvers, Reluplex: a calculus for reasoning about deep neural networks, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Combining decision procedures by (model-)equality propagation, Being careful about theory combination, Resolution proof transformation for compression and interpolation, Deciding floating-point logic with abstract conflict driven clause learning, An efficient SMT solver for string constraints, Combining Decision Procedures by (Model-)Equality Propagation, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Conflict-driven satisfiability for theory combination: transition system and completeness, Colors Make Theories Hard, SPASS-SATT. A CDCL(LA) solver, A complete and terminating approach to linear integer solving, A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, 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, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Reasoning about vectors using an SMT theory of sequences