Deciding effectively propositional logic using DPLL and substitution sets

DOI10.1007/s10817-009-9161-6zbMath1197.03011OpenAlexW1999468161MaRDI QIDQ972432

Nikolaj Bjørner, Leonardo de Moura, Ruzica Piskac

Publication date: 26 May 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9161-6

zbMATH Keywords

SATDPLLBDDSeffectively propositional logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Automated Reasoning Building Blocks, Ensuring Correctness of Model Transformations While Remaining Decidable, Feferman-vaught decompositions for prefix classes of first order logic, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Property Directed Reachability for Proving Absence of Concurrent Modification Errors, Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment, On the verification of security-aware E-services, Semantically-guided goal-sensitive reasoning: inference system and completeness, Deciding effectively propositional logic using DPLL and substitution sets, Unnamed Item, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, SCL clause learning from simple models, A complete and terminating approach to linear integer solving, SGGS decision procedures

Uses Software

• MiniSat
• Darwin

Cites Work

• Unnamed Item
• Deciding effectively propositional logic using DPLL and substitution sets
• Complexity results for classes of quantificational formulas
• The model evolution calculus as a first-order DPLL method
• Boolean expression diagrams
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Proof Systems for Effectively Propositional Logic
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Graph-Based Algorithms for Boolean Function Manipulation
• Theory and Applications of Satisfiability Testing
• Lemma Learning in the Model Evolution Calculus
• Programming Languages and Systems
• Theory and Applications of Satisfiability Testing