Revised U-evaluate([F])
Uses ToDo list of subproblems
- Initially ToDo = [ F ]
- Succeed when ToDo empty
Removes element G of ToDo list
Call E-evaluate(G)
- fail if E-evaluate fails
- if E-evaluate succeeds ...
- for each unsat soft clause returned
- assign universals so as to unsatisfy the soft clause
- add the resulting simplified problem to ToDo
- Return result of U-evaluate on revised ToDo list