Course talk:CPSC522/Conflict-Driven Clause Learning for the Boolean Satisfiability Problem

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

Critique from Gudbrand:

A nice introduction to some SAT-solver algos. The "Related Pages" section does a really good job of placing the article in the right context for the course. Some small comments: - The "complete" part of "NP-complete" should not be mathematically typeset. - In the text you write "discovered proved". I think an "and" is missing. - In the text somewhere: "box denote". Missing an "s" - In the text somewhere: "path the". Missing an "to" - Says the article builds on first order logic. I think zeroth order, i.e. propositional logic should be enough. - Perhaps mention in the beginning that the article also builds on some knowledge of "Theory of Computation". Some of the comments in the article assume the reader is comfortable with it. - You write: "have no barring". Should be "have no bearing"

The text flows nicely and is instructive to read. However I'm not sure how completely the papers themselves are presented (I haven't read them). It's a bit unclear sometimes what is background material and what is the contribution of the papers. I found the ending to be a bit abrupt. Perhaps a final section to wrap things up and zoom out on the line of research would help. Some sentences, such as the ones about "NP-completeness and purely experimental performance increase" and "100% failure rate vs. 0% failure rate" could be elaborated on. Assuming the reader hasn't (and won't) read the paper is reasonable.

The topic is relevant for the course. 5 The writing is clear and the English is good. 4 The page is written at an appropriate level for CPSC 522 students (where the students have diverse backgrounds). 4 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. 5 There was appropriate use of (pseudo-) code. 4 It had a good coverage of representations, semantics, inference and learning (as appropriate for the topic). 5 It is correct. 5 It was neither too short nor too long for the topic. 4 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. 4 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. 4 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