问数独- SAT的实现

EN

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

static List<List<Integer>> exactlyOneDigitForEachEntry() {
    ArrayList<Pair> pairs = Combinatorics.product(DIGITS);
    List<List<Integer>> clauses = new ArrayList();
    for (Pair pair : pairs) {
        ArrayList<Integer> literals = new ArrayList();
        for (int k : DIGITS) {
            int literal = (100 * pair.getA()) + (10 * pair.getB()) + k;
            literals.add(literal);
        }
        List<List<Integer>> 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<List<Integer>> exactlyOneOf(ArrayList<Integer> literals) {
    // The arrayList represents a boolean formula F such that F = true iff
    // there is exaclty one literal l such that l = true
    List<List<Integer>> expression = new ArrayList();
    expression.add(literals);
    ArrayList<Pair> pairs = Combinatorics.combinations(literals);
    for (Pair pair : pairs) {
        List<Integer> clause = new ArrayList();
        clause.add(-1 * pair.getA());
        clause.add(-1 * pair.getB());
        expression.add(clause);
    }
    return expression;
}