Hard and Soft Clauses

• Soft Clauses

  • clauses that can be left unsolved on this attempt
  • have some free universal variables
  • e.g. U or V or W or E
  • if we set E = false, have solution when U/V/W true
  • next test we set U=V=W=false and force new solution

• Hard Clauses

  • clauses that must be solved for problem to be soluble
  • i.e. No universal variables, e.g. E

Previous slide

Next slide

Back to first slide

View graphic version