Extended resolution simulates binary decision diagrams

We prove that binary decision diagrams [1] can be polynomially simulated by the extended resolution rule of [2]. More precisely, for any unsatisfiable formula , there exists an extended resolution refutation of where the number of steps is polynomially bounded by the maximal size of the BDDs built from the formulae occurring in . Key words: Extended Resolution, Binary Decision Diagrams

• Type: Journal
• Year: 2008
• Where: DAM
• Authors: Nicolas Peltier
• Keywords: Binary Decision, DAM 2008, Extended Resolution, Extended Resolution Rule