Equivalent literal propagation in the DLL procedure

DOI10.1016/S0166-218X(02)00407-9zbMath1029.68080MaRDI QIDQ1408382

Chu-Min Li

Publication date: 15 September 2003

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

zbMATH Keywords

SATDavis-Logemann-Loveland procedureEquivalency reasoning

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items (1)

Generating Extended Resolution Proofs with a BDD-Based SAT Solver

Uses Software

• SatEx
• SATO
• Chaff
• DIMACS
• HeerHugo
• ZRes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Explicit constructions of linear-sized superconcentrators
• A two-phase algorithm for solving a class of hard satisfiability problems
• The propositional formula checker HeerHugo
• Hard examples for resolution
• SATO: An efficient propositional prover
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• Principles and Practice of Constraint Programming – CP 2003

This page was built for publication: Equivalent literal propagation in the DLL procedure