I avoided Sudoku for as long as possible because I knew what would happen but I finally succumbed, so here is the resulting logic-only (no guessing) Javascript Sudoku helper/solver: http://www.mathstat.dal.ca/~jpg/sudoku/ As far as I can tell this is currently the most powerful online solver. Back in November there was some discussion as to what qualifies as "no guessing"; Bernie Cosell opined that if multiple implication chains are used to establish a single condition then this is a form of guessing since it essentially tries a number antecedents in turn. Sudoku Helper uses implication chains which are of the form (d not in A) => (x1 in X1) => (x2 not in X2) => (x3 in X2) => ... => (d in B) Which simplifies to (d not in A) => (d in B), which is the same as "d is in A or B". Many of the existing strategies are of this form (i.e. they show that a single digit must be in a set of squares and use this fact to eliminate possibilities), so I feel fairly comfortable in classifying this as a logic technique rather than a guessing technique. More generally, any unsolved Soduku puzzle can be turned into formal logic using a set of predicates A_d ("The digit d is in the square A"), and a set of constraints defined by the rules of Sudoku and the current position (e.g. (A_2 v A_3 v A_7)). One could then write a theorem prover whose search algorithm is customized for Sudoku; the theorem prover could also avoid "proof by contradiction". At that point it becomes hard to argue that anything but logic is being used, even if the prover is doing things like merging multiple implication chains in a way that, for a human, would be guessing. It all boils down to semantics, and I would have to say that "guessing" really means "logic that doesn't fit in a human's head". J.P.