Abstract DPLL and abstract DPLL modulo theories
From MaRDI portal
Recommendations
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- An abstract interpretation of DPLL(T)
- A DPLL-based calculus for ground satisfiability modulo theories
- DPLL(T): Fast decision procedures
- An Abstract Framework for Satisfiability Modulo Theories
Cited in
(28)- Constructing cycles in the simplex method for DPLL(T)
- A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
- On integer closure in a system of unit two variable per inequality constraints
- Propagation via lazy clause generation
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Generalizing DPLL and satisfiability for equalities
- Integer feasibility and refutations in UTVPI constraints using bit-scaling
- FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
- A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
- Deduction, strategies, and rewriting
- An abstract interpretation of DPLL(T)
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- Satisfiability modulo theories
- Extracting a DPLL algorithm
- MathCheck: a math assistant via a combination of computer algebra systems and SAT 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
- Propagation = Lazy Clause Generation
- From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain
- A DPLL-based calculus for ground satisfiability modulo theories
- Lifting CDCL to template-based abstract domains for program verification
- Ground Interpolation for Combined Theories
- Using membrane calculus to describe DPLL algorithm with clause learning
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- Quo Vadis Answer Set Programming?
- Computer Aided Verification
- MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)
- \texttt{flingo} -- instilling ASP expressiveness into linear integer constraints
This page was built for publication: Abstract DPLL and abstract DPLL modulo theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5705940)
