Will Nowak made several wrong statements on Friday Nov. 20, 2009. Let me correct them. Statement 1 (from memory): This course does not give us opportunities to practice design. We were given a basic player to start with where all the design work was already done. ----------------------------- Response 1: This course creates design opportunities but does not force them on you. There is plenty of design work that goes into a good solver. For example, the SAT4J MAXSAT solver contains hundreds of classes. See: http://www.sat4j.org/maven21/org.sat4j.maxsat/dependencies.html org.sat4j.core-2.1.0.jar 207.52 kB 154 classes http://www.sat4j.org/ the SAT4J library is only 400Kb big. You have the opportunity to design plenty of useful classes for your solver if you want to. You design the solver that fits into your skill and time budget. Statement 2 by Will Nowak (from memory): This course forces us to solve unsolvable problems which is ridiculous. We don't learn anything from solving academic problems that have no practical relevance. ----------------------------- Response 2: MAX-CSP (which includes SAT, MAXSAT) solvers deal with those problems on a routine basis. Even the Eclipse tool, that many students use, includes a SAT and MAXSAT and pseudo-boolean solver. See below. It is wrong to say that MAX-CSP is unsolvable. Unsolvable has a precise technical meaning. The Halting problem or the grammar ambiguity problem are unsolvable. MAX-CSP is solvable but it is NP-hard. March 24, 2009: Millions of SAT4J users worldwide? SAT4J ships in Eclipse 3.4. Here are some public numbers regarding the number of downloads of Eclipse distributions on Eclipse.org web site since June 2008. Note that those numbers do not include third party products such as IBM or Genuitec ones based on Eclipse. Ganymede (Eclipse 3.4, SAT4J 2.0.0) around 3M downloads. May 2009: SAT4J 2.1 released A new release of SAT4J is now available. It will ship with Eclipse 3.5 (Galileo). The 2.1 release facilitates the integration of SAT technology in Java software, and improves the optimization engines (PB, MAXSAT). http://mail-archive.ow2.org/sat4j-dev/2008-03/msg00001.html Eclipse now includes a copy of SAT4J (namely the core and pseudo boolean parts). In Eclipse, SAT4J is part of new provisioning mechanism, where it constitutes the cornerstone of the dependency management of plug-in installation, putting to use the ideas described in [1] and [2]. http://www.maxsat.udl.cat/08/ms08-pres.pdf MAX-SAT competition 2008 Statement 3 by Will Nowak: This is the only class where someone has to get an F for someone else to get an A. ----------------------------- Response 3: This statement is wrong. Let's assume 3 agents A, B, C. A beats B, B beats C, C beats A. All three beat the BasicPlayer. All three agents get an A. Remember "beats" means "finds bugs".