Function E-Evaluate(F)

• If clause set is empty, succeed

• If there is empty/all universal clause, fail

• Try Davis-Putnam on Existential Simplification

  • If this solves all clauses, succeed

• Apply Propagation rules

• If the outermost quantifier is now Universal

  • Return result of U-evaluate(F)

• Choose a E-variable e

  • Succeed if E-Evaluate(F e:=true) succeeds
  • Else return result of E-Evaluate(F e:=false)

Previous slide

Next slide

Back to first slide

View graphic version