Generalizing DPLL and satisfiability for equalities

Bahareh Badban, Jan Cornelis van de Pol, Olga Tveretina, Hans Zantema

    Research output: Contribution to journalArticleAcademicpeer-review

    7 Citations (Scopus)
    118 Downloads (Pure)


    We present GDPLL, a generalization of the DPLL procedure. It solves the satisfiability problem for decidable fragments of quantifier-free first-order logic. Sufficient conditions are identified for proving soundness, termination and completeness of GDPLL. We show how the original DPLL procedure is an instance. Subsequently the GDPLL instances for equality logic, and the logic of equality over infinite ground term algebras are presented. Based on this, we implemented a decision procedure for inductive datatypes. We provide some new benchmarks, in order to compare variants.
    Original languageEnglish
    Pages (from-to)1188-1211
    Number of pages24
    JournalInformation and computation
    Issue numberLNCS4549/8
    Publication statusPublished - Aug 2007


    • DPLL procedure
    • Decision procedure
    • Inductive datatypes
    • Ground term algebra
    • Satisfiability
    • EWI-11281
    • CR-I.2.3
    • Equality


    Dive into the research topics of 'Generalizing DPLL and satisfiability for equalities'. Together they form a unique fingerprint.

    Cite this