Davis Putnam Algorithm for SAT

• If any clause false, fail

• If all clauses satisfied, succeed

• If any clause is unit, set the relevant variable, recurse

• Otherwise

  • set any variable to true and recurse

    • if result is success, succeed
    • if result is failure,

      • set the variable to false and recurse

Previous slide

Next slide

Back to first slide

View graphic version