Machine-translated by Google. Questions are authored in English.
Top

Discussion

What is conflict driven clause learning?

  • A.Deriving all consequences of the clauses before searching
  • B.Deriving a new clause from each conflict to prevent its recurrence
  • C.Learning which variables to assign first from experience
  • D.Recording every assignment that has been tried and failed

Answer: B

When a conflict occurs, analysing the implication graph yields a clause capturing the cause, which is added permanently and prevents the same combination from being explored again. With restarts it transformed satisfiability solving from thousands to millions of variables. Variable ordering, exhaustive recording and preprocessing are different techniques. Converting a failure into a permanent constraint is the same idea as no-good learning in constraint solving, arrived at independently.

No comment is present. Be the first to comment.
Loading…

Post your comment

Please log in or register to post a comment.