DPLL(T): Fast decision procedures
From MaRDI portal
DPLL(\(T\)): Fast decision procedures
Recommendations
- Computer Aided Verification
- EufDPLL -- a tool to check satisfiability of equality logic formulas
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- A decision procedure for equality logic with uninterpreted functions
- Generalizing DPLL and satisfiability for equalities
Cited in
(67)- 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
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Dashed strings for string constraint solving
- Subsumption demodulation in first-order theorem proving
- Automated generation of exam sheets for automated deduction
- The SAT+CAS method for combinatorial search with applications to best matrices
- SPASS-SATT. A CDCL(LA) solver
- Applying computer algebra systems with SAT solvers to the Williamson conjecture
- SMELS: satisfiability modulo equality with lazy superposition
- A decision procedure for (co)datatypes in SMT solvers
- Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
- Efficient theory combination via Boolean search
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
- Generalizing DPLL and satisfiability for equalities
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
- The taming of the (X)OR
- Rewrite-based decision procedures
- Generating minimum transitivity constraints in P-time for deciding equality logic
- Model-based theory combination
- Proof tree preserving tree interpolation
- Distributing the workload in a lazy theorem-prover
- Decision procedures for region logic
- An abstract interpretation of DPLL(T)
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Weakly equivalent arrays
- Solving finite-domain linear constraints in presence of the $\texttt{alldifferent}$
- A Lambda-Free Higher-Order Recursive Path Order
- Encoding OCL data types for SAT-based verification of UML/OCL models
- Satisfiability modulo theories
- A decision procedure for (co)datatypes in SMT solvers
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
- From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Generalizing DPLL to Richer Logics
- Combining equational reasoning
- Deciding floating-point logic with abstract conflict driven clause learning
- Harald Ganzinger's legacy: contributions to logics and programming
- Parametrized invariance for infinite state processes
- EufDPLL -- a tool to check satisfiability of equality logic formulas
- A search-based procedure for nonlinear real arithmetic
- Decision procedures. An algorithmic point of view
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
- Disequality management in integer difference logic via finite instantiations.
- An experimental evaluation of ground decision procedures
- A decision procedure for equality logic with uninterpreted functions
- Logic for Programming, Artificial Intelligence, and Reasoning
- Computer Aided Verification
- LATIN 2004: Theoretical Informatics
- Synthesising programs with non-trivial constants
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
- A \textit{DPLL} procedure with dichotomous branching for propositional product logic
- Computing ground congruence classes
- Extensions of the cylindrical algebraic covering method for quantifiers
- SCIP: solving constraint integer programs
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Applying SAT solving in classification of finite algebras
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- Fast congruence closure and extensions
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
- Automatic construction and verification of isotopy invariants
- CPBPV: a constraint-programming framework for bounded program verification
- Deciding effectively propositional logic using DPLL and substitution sets
This page was built for publication: DPLL(\(T\)): Fast decision procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5312898)
