Critique 2

Comments

Overall it provides a nice summary of SAT solving and the two algorithms (DPLL and CDCL) discussed in the papers. The series of diagrams illustrating the branching of the variable assignments is excellent. The only part that is a little confusing and feels rushed is in the "Backjumping" section of the CDCL discussion. While the mechanics of back-jumping is pretty clear, the use of the word reason is not (does it have the common meaning of the word reason or is it referring to a specific clause in a certain context?).

Also I think there is a typo in "Backjumping" section (I might be wrong):

• However, eventually, we will need to exclude $c\equiv \top$ as well because of $(a\lor b\lor c)$ and we obtain a contradiction.

Should be:

• However, eventually, we will need to exclude $c\equiv \top$ as well because of $(a\lor b\lor \lnot c)$ and we obtain a contradiction.

Scheme

• The topic is relevant for the course. 5
• The writing is clear and the English is good. 5
• The page is written at an appropriate level for CPSC 522 students (where the students have diverse backgrounds). 5
• The formalism (definitions, mathematics) was well chosen to make the page easier to understand. 5
• The abstract is a concise and clear summary. 5
• There were appropriate (original) examples that helped make the topic clear. 4
• There was appropriate use of (pseudo-) code. 2
• It had a good coverage of representations, semantics, inference and learning (as appropriate for the topic). 4
• It is correct. 5
• It was neither too short nor too long for the topic. 5
• It was an appropriate unit for a page (it shouldn't be split into different topics or merged with another page). 5
• It links to appropriate other pages in the wiki. -
• The references and links to external pages are well chosen. 4
• I would recommend this page to someone who wanted to find out about the topic. 5
• This page should be highlighted as an exemplary page for others to emulate. 4
• If I was grading it out of 20, I would give it: 16