Solves a simplified version of sudoku (w/ only row and column constraints) using z3 SAT solver

simpleSudokuSolver.groovy

/*
 * Copyright (c) 2018, Venkatesh-Prasad Ranganath
 *
 * Licensed under BSD 3-clause License
 *
 * Author: Venkatesh-Prasad Ranganath
 */

// Solves a simplified version of sudoku (w/ only row and column constraints)
// using SAT solving
// Script uses z3 solver (https://github.com/Z3Prover/z3)

final cli = new CliBuilder(usage:"groovy simpleSudokuSATSolver.groovy")
cli.n(longOpt:'gridWidth', args:1, argName:'gridWidth', required:true,
    'Grid width.  Grid height will be the same.')
cli.s(longOpt:'z3Path', args:1, argName:'z3Path', required:true,
    'Path to z3')
final options = cli.parse(args)
if (!options) {
    return
}

// Output specifies the cells in which n copies of n numbers need to be placed

// Every cell has at least one value

// Every cell has at most one value

// Every row has at least one instance of every value

// Every col has at least one instance of every value

final n = options.n as int

final cellAndValue2var = { ->
    final tmp1 = [:]
    tmp1.withDefault { tmp1.size() + 1 }
}.call()

final formula = []

// Every cell has at least one value
formula.addAll([1..n, 1..n].combinations().collect { row, col ->
    (1..n).collect { cellAndValue2var["$row, $col, $it"] }
})

// Every cell has at most one value
formula.addAll([1..n, 1..n].combinations().collectMany { row, col ->
    (1..n).inject([]) { acc, val1 ->
        final var1 = cellAndValue2var["$row, $col, $val1"]
        final clause = (1..n).findAll { it > val1 }.collect { val2 ->
            final var2 = cellAndValue2var["$row, $col, $val2"]
            [-var1, -var2]
        }
        acc.addAll(clause)
        return acc
    }
})

// Every row has at least one instance of every value
formula.addAll([1..n, 1..n].combinations().collect { row, val ->
    (1..n).collect { col -> cellAndValue2var["$row, $col, $val"] }
})

// Every col has at least one instance of every value
formula.addAll([1..n, 1..n].combinations().collect { col, val ->
    (1..n).collect { row -> cellAndValue2var["$row, $col, $val"] }
})

// Place few values at random positions
println "Random placements"
[1..n, 1..n, 1..n].combinations().sort { Math.random() }
        .take(n).each { r, c, v ->
    final place = "$r, $c, $v"
    formula.add([cellAndValue2var[place]])
    println place
}

final file = new File("simpleSudoku.cnf")

file.withPrintWriter { writer ->
    final tmp1 = formula.collect { clause -> clause.sort(Math.&abs) }.unique()
    writer.println "p cnf ${cellAndValue2var.size()} ${tmp1.size()}"
    tmp1.each {
        writer.println it.join(' ') + ' 0'
    }
}

final process = ("${options.s} " + file.name).execute()
final outStream= process.getInputStream()
process.waitFor()
final output = outStream.readLines()

if (output[0] == 'sat') {
    final tmp1 = cellAndValue2var.collectEntries { k, v -> [v, k] }
    println "Row, Col, Value"
    output[1].split(' ').collect { it as int }.findAll { it > 0 }.each {
        println tmp1[it]
    }
} else
    println 'unsat'