Depth First Search for SAT

• What heuristics should we use?

• We need two kinds

  • variable ordering
    • e.g. set A before B
  • value ordering
    • e.g. set True before False

• In Eights, only need value

  • variable ordering irrelevant

• In SAT, variable ordering vital

  • value ordering less important

Previous slide

Next slide

Back to first slide

View graphic version