Sudoku Solver To SAT implementation I implemented an algorithm for solving sudoku using reduction from sudoku to SAT.    

Now, I am trying to refactor the code using code review principles. I find some difficulties apply the principles. Because of that I would like to share the following code snippet in order to get some hints how to approach this problem efficiently.

The following method generate boolean expressions in CNF such that for any entry puzzle_{ij} a boolean expression E in CNF will be generated such that E = true iff there is exactly one literal x_{ijk}, k in {1, 2, ..., 9} such that x_{ijk} = true

// DIGITS := {1, 2, ..., 9}
// Combinatorics.product(DIGITS) = {(1,1), (1,2), ..., (9,8), (9,9)}

static List&lt;List&lt;Integer&gt;&gt; exactlyOneDigitForEachEntry() {
    ArrayList&lt;Pair&gt; pairs = Combinatorics.product(DIGITS);
    List&lt;List&lt;Integer&gt;&gt; clauses = new ArrayList();
    for (Pair pair : pairs) {
        ArrayList&lt;Integer&gt; literals = new ArrayList();
        for (int k : DIGITS) {
            int literal = (100 * pair.getA()) + (10 * pair.getB()) + k;
            literals.add(literal);
        }
        List&lt;List&lt;Integer&gt;&gt; expression = exactlyOneOf(literals);
        extendClauses(clauses, expression);
    }

    return clauses;
}


.

/**
 *
 * @param literals A set of literals
 * @return a boolean expression E in conjunctive normal form such that E =
 * true iff there is exactly one literal that is true.
 */
private static List&lt;List&lt;Integer&gt;&gt; exactlyOneOf(ArrayList&lt;Integer&gt; literals) {
    // The arrayList represents a boolean formula F such that F = true iff
    // there is exaclty one literal l such that l = true
    List&lt;List&lt;Integer&gt;&gt; expression = new ArrayList();
    expression.add(literals);
    ArrayList&lt;Pair&gt; pairs = Combinatorics.combinations(literals);
    for (Pair pair : pairs) {
        List&lt;Integer&gt; clause = new ArrayList();
        clause.add(-1 * pair.getA());
        clause.add(-1 * pair.getB());
        expression.add(clause);
    }
    return expression;
}
The code is pretty short, so there's not much to comment on.

Magic numbers

int literal = (100 * pair.getA()) + (10 * pair.getB()) + k


I have no idea what that means. What is 100? What is 10? Why do you sum them up? I suggest creating a method int getLiteralId(int firstDigit, int secondDigit, int thirdDigit) and add a comment that explains what's actually going on.

clause.add(-1 * pair.getA());
clause.add(-1 * pair.getB());


Why are multiplying them by -1? At least create a method with an appropriate name (something like int negateLiteral(int literalId)).

Variable names

k and pairs isn't very descriptive. I suggest something like digit and digitPairs.

Overall design

Representing a boolean expression as a list of integers leads to confusion. I'd redesign it in the following way: 


A BooleanExpression abstract base class.
A Variable subclass for representing variables.
A Negation subclass for representing negations.
A Conjunction subclass for representing  conjunctions.
A Disjunction subclass for representing disjunctions.
The signatures will be
BooleanExpression exactlyOneOf(List&lt;BooleanExpression&gt; expressions) and
BooleanExpression exacltyOneDigitForEachEntry()  


It'll make the code much more readable. For instance,

Conjunction conjunction = new Conjunction();
...
conjunction.add(new Negation(expression));


and 

Disjunction disjunction = new Disjunction();
disjunction.add(new Variable(firstDigit));
disjunction.add(new Variable(secondDigit));
disjunction.add(new Variable(thirdDigit));
conjunction.add(disjunction);


looks much better than some "magic" multiplication and addition of seemingly unrelated numbers, doesn't it?

It's safer in a sense that an arbitrary integer can't accidentally turn into a literal/expression.

It also makes more sense because a boolean expression is a boolean expression. It's not a list of integers (it might be implemented as such, but it's an implementation detail).

What if you use a third-party solver and it needs a list of integers in a specific format?  It doesn't really matter. You can still use the design shown above. Just add a toList method to the BooleanExpression and implement it in concrete subclasses according to the rules of the solver. Call it only once before passing your expression to the solver.