Deciding effectively propositional logic using DPLL and substitution sets
type: Item
instance of: scholarly article
title: Deciding effectively propositional logic using DPLL and substitution sets
zbMATH Open document ID: 1197.03011
author: Ružica Piskač
author: Leonardo de Moura
author: Nikolaj Bjørner
published in: Journal of Automated Reasoning
publication date: 2010-05-26T00:00:00Z
review text: This paper introduces a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also called EPR. This class of first-order formulas provides a generalization of pure propositional satisfiablility and quantified Boolean formulas. The presented DPLL calculus is complete in EPR and combines techniques for efficient propositional search, such as Binary Decision Diagrams. The calculus works directly at the level of sets and it is opened up to efficient implementations based on data structures, with promising preliminary empirical results.
reviewed by: Emilio Muñoz-Velasco
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5711944
zbMATH Keywords: DPLL
zbMATH Keywords: SAT
zbMATH Keywords: BDDS
zbMATH Keywords: effectively propositional logic
describes a project that uses: Darwin
describes a project that uses: MiniSat
MaRDI profile type: Publication
full work available at URL: s10817-009-9161-6
OpenAlex ID: W1999468161
cites work: Boolean expression diagrams
cites work: Lemma Learning in the Model Evolution Calculus
cites work: The model evolution calculus as a first-order DPLL method
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
cites work: Geometric Resolution: A Proof Procedure Based on Finite Model Search
cites work: Theory and Applications of Satisfiability Testing
cites work: Resolution decision procedures
cites work: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
cites work: Complexity results for classes of quantificational formulas
cites work: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
cites work: Proof Systems for Effectively Propositional Logic
cites work: Programming Languages and Systems
DOI: 10.1007/S10817-009-9161-6
description: scientific article; zbMATH DE number 5711944