Failure Driven Search

• Any partial solution (e.g. from DP) is helpful ...

  • ... as long as it solves all clauses without universals

• The existential assignment solves many clauses

  • applies to all universal assignments ...
  • except those invalidating universals in unsat clauses

• Future tests need only solve remaining cases

• Failure-driven rather than blind search

• Exploits work done by failed calls to DP

Previous slide

Next slide

Back to first slide

View graphic version