Identifies a queue-based BFS traversal order of nodes of a given directed graph using z3 solver

bfsSolver2.groovy

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

import groovy.transform.Field

// Identifies a BFS traversal order of nodes of a given directed graph
// using SAT solving
// Script uses z3 solver (https://github.com/Z3Prover/z3)

final cli = new CliBuilder(usage:"groovy dfsSolver.groovy")
cli.s(longOpt:'z3Path', args:1, argName:'z3Path', required:true,
        'Path to z3')
cli.g(longOpt:'graph', args:1, argName:'graph', required:true,
        'Directed Graph to traverse. Each line is an edge in "n1,n2" format')
final options = cli.parse(args)
if (!options) {
    return
}

// In BFS, from a source node, every reachable node is visited in levels/layers.

// Output is an ordering of |N| nodes

// Each node occurs in at least one position

// Each node occurs in at most one position

// Each position has at least one node

// For each edge (m, n), if m@g, n@h, and g<h,
// then, for each node q@j such that g<j<h, there exists an edge (p, q) such
//   that p@i and i<=g

final edges = new File(options.g).readLines().collect {
    it.split(',') as List
}
final nodes = edges.collectMany { it }.unique()
final positions = 1..nodes.size()

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

@Field final nodePos2var = [:].withDefault { varMap[it] }
def getVarForNodePos(n, l) { nodePos2var["$n,$l"] }

final formula = []

// Each node occurs in at least one position
final subFormula1 = nodes.collect { n ->
    positions.collect { l -> getVarForNodePos(n, l) }
}
formula.addAll(subFormula1)

// Each node occurs in at most one position
final subFormula2 = [nodes, positions].combinations()
        .collectMany { n, l ->
    final v1 = getVarForNodePos(n, l)
    positions.findAll { it > l }.collect { k ->
        [-v1, -getVarForNodePos(n, k)]
    }
}
formula.addAll(subFormula2)

// Each position has at least one node
final subFormula3 = positions.collect { g ->
    nodes.collect { n -> getVarForNodePos(n, g) }
}
formula.addAll(subFormula3)

// For each edge (m, n), if m@g, n@h, and g<h,
// then, for each node q@j such that g<j<h, there exists an edge (p, q) such
//   that p@i and i<=g
List combinations(List list) {
    list.any { it.empty } ? [] : list.combinations()
}

final subFormula4 = edges.collectMany { m, n ->
    [positions, positions].combinations().findAll { it[0] < it[1] }
            .collectMany { g, h ->
        final mAtg = getVarForNodePos(m, g)
        final nAth = getVarForNodePos(n, h)
        combinations([nodes.findAll { it != m && it != n },
                      positions.findAll { it > g && it < h }])
                .collect { q, j ->
            final qAtj = getVarForNodePos(q, j)
            final tmp1 = edges.findAll { it[1] == q }.collect { it[0] }
            final tmp2 = positions.findAll { it <= g }
            final tmp3 = combinations([tmp1, tmp2])
            [-mAtg, -nAth, -qAtj] +
                    tmp3.collect { p, i -> getVarForNodePos(p, i) }
        }
    }
}
formula.addAll(subFormula4)

// Pick a random starting node
final startNode = nodes[new Random().nextInt(nodes.size())]
formula.add([getVarForNodePos(startNode, 1)])

final file1 = new File("bfsGraphOrder.cnf")

file1.withPrintWriter { writer ->
    final tmp1 = formula.unique { it.sort().join() }
    writer.println "p cnf ${nodePos2var.size()} ${tmp1.size()}"
    tmp1.each {
        writer.println it.join(' ') + ' 0'
    }
}

final process1 = ("${options.s} " + file1.name).execute()
final outStream1 = process1.getInputStream()
process1.waitFor()
final output1 = outStream1.readLines()

if (output1[0] == 'unsat') {
    println 'unsat'
    System.exit(0)
}

final var2nodePos = nodePos2var.collectEntries { k, v -> [v, k] }
println "Node,Pos"
output1[1].split(' ').collect { it as int }.findAll { it in var2nodePos }
        .collect { var2nodePos[it].split(',') }.sort { it[1] as int }
        .each { println it.join(',') }