Generalizing DPLL and satisfiability for equalities

DOI10.1016/J.IC.2007.03.003MaRDI QIDQ2643080zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Bahareh Badban, Jaco van de Pol, Olga Tveretina, Hans Zantema

Publication date 23 August 2007

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2007.03.003

zbMATH Keywords

decision procedureDPLL procedureequalityground term algebrainductive datatypessatisfiability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• DPLL(T): Fast decision procedures
• Generalizing DPLL to Richer Logics
• A DPLL-based calculus for ground satisfiability modulo theories
• Abstract DPLL and abstract DPLL modulo theories
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cites work

• A Computing Procedure for Quantification Theory
• A decision procedure for equality logic with uninterpreted functions
• A framework for cooperating decision procedures
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A SAT based approach for solving formulas over Boolean and linear mathematical propositions
• Algebraic process verification.
• BDD based procedures for a theory of equality with uninterpreted functions
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Combining Shostak theories
• Congruence closure with integer offsets
• CVC: A cooperating validity checker
• Deciding equality formulas by small domains instantiations
• DPLL(T): Fast decision procedures
• Equational binary decision diagrams
• Equational problems and disunification
• Exploiting positive equality in a logic of equality with uninterpreted functions
• FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
• Generalizing DPLL and satisfiability for equalities
• scientific article; zbMATH DE number 4053011 (Why is no real title available?)
• ICS: Integrated canonizer and solver
• On the complexity of equational problems in CNF
• SAT-based decision procedures for automated reasoning: A unifying perspective
• Solvable cases of the decision problem
• Transforming equality logic to propositional logic
• Zero, successor and equality in BDDs

Cited in

(9)

• Generalizing DPLL and satisfiability for equalities
• FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
• Computing All Implied Equalities via SMT-Based Partition Refinement
• Generalized Davis-Putnam and satisfiability problems in mathematics
• Generalizing DPLL to Richer Logics
• Deciding floating-point logic with abstract conflict driven clause learning
• Deciding equality formulas by small domains instantiations
• EufDPLL -- a tool to check satisfiability of equality logic formulas
• DPLL(T): Fast decision procedures

Describes a project that uses

Uses Software

• ATERM
• ICS
• mCRL
• CVC

This page was built for publication: Generalizing DPLL and satisfiability for equalities

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