Cadoli et al's Evaluate algorithm
Two mutually recursive functions
- U-evaluate for universal quantifiers
- E-evaluate for existential quantifier
Many propagation rules in each
- e.g. `unit propagation'
- If a clause exists with only a single existential literal
- ... commit to the E-variable having the relevant value
I will not detail propagation rules
Focus on branching nature of search ...
... and an unusual preprocessing step