Function U-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 Existential

  • Return result of E-evaluate(F)

• Choose a U-variable u

  • Fail if U-Evaluate(F u:=true) fails
  • Else return result of U-Evaluate(F u:=false)

Previous slide

Next slide

Back to first slide

View graphic version