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

Discussion

What is the watched literal technique?

  • A.Keeping a list of the literals assigned at each decision level
  • B.Monitoring two literals per clause to detect unit and conflict states
  • C.Recording which literals appear most often across the formula
  • D.Observing which literals cause the most conflicts during search

Answer: B

Watching two unassigned literals per clause means a clause need only be inspected when one of its watches is falsified, which avoids visiting every clause on every assignment. It is the single most important implementation trick in a modern solver. Frequency, conflict statistics and assignment stacks are different mechanisms. An implementation technique that changes the constant factor by an order of magnitude deserves to be named alongside the algorithmic ideas.

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

Post your comment

Please log in or register to post a comment.