Sorts three numbers by encoding the sorting problem as a SAT problem

3NumSorter.groovy

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

// Sorts three numbers using SAT solving
// Script uses z3 solver (https://github.com/Z3Prover/z3)

final cli = new CliBuilder(usage:"groovy 3NumSorter.groovy")
cli.n(longOpt:'numbers', args:1, argName:'numbers', required:true,
    'Comma separated list of three numbers to sort.')
cli.s(longOpt:'z3Path', args:1, argName:'z3Path', required:true,
    'Path to z3')
final options = cli.parse(args)
if (!options) {
    return
}

// Output will have three numbers in three positions.

// Each number should occur in at least one position

// Each number should occur in at most one position

// Each position should contain at least one number

// Each position should contain at most one number

// If x occurs at position m, y occurs at position n, and m=n-1,
// then x <= y

final nums = options.n.split(',')[0..2]

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

final formula = []

// Each number should occur in at least one position
final subFormula1 = (1..3).collect { x ->
    (1..3).collect { m -> varMap["vN${x}P$m"] }
}
formula.addAll(subFormula1)

// Each number should occur in at most one position
final subFormula2 = (1..3).collectMany { x ->
    [1..3, 1..3].combinations().findAll { it[0] != it[1] }.collect { m, n ->
        [-varMap["vN${x}P$m"], -varMap["vN${x}P$n"]]
    }
}
formula.addAll(subFormula2)

// Each position should contain at least one number
final subFormula3 = (1..3).collect { m ->
    (1..3).collect { x -> varMap["vN${x}P$m"] }
}
formula.addAll(subFormula3)

// Each position should contain at most one number
final subFormula4 = (1..3).collectMany { m ->
    [1..3, 1..3].combinations().findAll { it[0] != it[1] }.collect { x, y ->
        [-varMap["vN${x}P$m"], -varMap["vN${y}P$m"]]
    }
}
formula.addAll(subFormula4)

// If x occurs at position m, y occurs at position n, and m=n-1,
// then x <= y
final subFormula5 = [1..3, 1..3].combinations().collectMany { x, y ->
    (1..2).collect { m ->
        final n = m + 1
        [-varMap["vN${x}P$m"], -varMap["vN${y}P$n"], varMap["vN${x}LN$y"]]
    }
}
formula.addAll(subFormula5)

// Add nx <= ny constraints
final subFormula6 = [1..3, 1..3].combinations().collect { x, y ->
    [varMap["vN${x}LN${y}"] * (nums[x - 1] <= nums[y - 1] ? 1 : -1)]
}
formula.addAll(subFormula6)

final file = new File("3numSorting.cnf")

file.withPrintWriter { writer ->
    final tmp1 = formula.collect { clause -> clause.sort(Math.&abs) }.unique()
    writer.println "p cnf ${varMap.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 = varMap.collectEntries { k, v -> [v, k] }
    println "Num,Pos"
    output[1].split(' ').collect { it as int }.findAll { it > 0 }
    .findAll { tmp1[it] ==~ /.*P.*/ }.each {
        final num = nums[(tmp1[it][2] as int) - 1]
        final pos = (tmp1[it][4] as int)
        println "$num,$pos"
    }
} else
    println 'unsat'