Extended resolution simulates binary decision diagrams

DOI10.1016/J.DAM.2006.11.012MaRDI QIDQ2478427zbMATH OpenOpenAlexFDO

Authors Nicolas Peltier

Publication date 28 March 2008

Published in Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.dam.2006.11.012

zbMATH Keywords

binary decision diagramsextended resolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Resolution and binary decision diagrams cannot simulate each other polynomially
• Extended Resolution Proofs for Conjoining BDDs
• scientific article; zbMATH DE number 2084326
• Extended resolution simulates \({\mathsf{DRAT}}\)
• Generating extended resolution proofs with a BDD-based SAT solver

Cites work

• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• An optimality result for clause form translation
• Computing small clause normal forms
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 1150567 (Why is no real title available?)
• scientific article; zbMATH DE number 1926658 (Why is no real title available?)
• scientific article; zbMATH DE number 3420722 (Why is no real title available?)
• On a generalization of extended resolution
• Resolution and binary decision diagrams cannot simulate each other polynomially
• The complexity of theorem-proving procedures
• The intractability of resolution
• The propositional formula checker HeerHugo
• The relative efficiency of propositional proof systems

Cited in

(8)

• Pool resolution is NP-hard to recognize
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Extended resolution simulates \({\mathsf{DRAT}}\)
• Generating extended resolution proofs with a BDD-based SAT solver
• Counting the number of equivalent binary resolution proofs
• scientific article; zbMATH DE number 2084326 (Why is no real title available?)
• Extended Resolution Proofs for Conjoining BDDs
• Using extended resolution to represent strongly connected components of directed graphs

Describes a project that uses

Uses Software

• HeerHugo

This page was built for publication: Extended resolution simulates binary decision diagrams

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