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

bfsSolver.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 a set of |N| node and level pairs.
// In the worst case, there can be |N| levels.

// Each node is associated with at least one level

// Each node is associated with at most one level

// If level l < |N| is empty (i.e., does not contain any node),
// then level l + 1 is empty

// If level l > 1 is not empty, then level l - 1 is not empty

// For every edge (m, n), if m occurs at level l,
// then n cannot occur at level k > l + 1

// If node m and n occur at level l, then
// there exists two edges (p, m) and (q, n) such that
// p and q occur at level l - 1

// Level 1 has at least one node

final rawEdges = new File(options.g).readLines().collect {
    it.split(',') as List
}
final rawNodes = rawEdges.collectMany { it }.unique()
final id2node = rawNodes.inject([:]) { acc, n -> acc[acc.size() + 1] = n ; acc}
final nodeIds = id2node.keySet()
final levels = 1..nodeIds.size()
final numLevels = levels.size()
@Field final varMap = { ->
    final tmp1 = [:]
    tmp1.withDefault { tmp1.size() + 1 }
}.call()

@Field final nodeIdLevel2var = [:].withDefault { varMap[it] }

def getVarForNodeIdAndLevel(nodeId, level) {
    nodeIdLevel2var["n$nodeId,l$level"]
}

@Field final nodeIdPair2var = [:].withDefault { varMap[it] }

def getVarForNodeIdPairAndLevel(m, n, l) {
    nodeIdPair2var['NN' + [m, n].sort(Math.&abs).join(',') + ",$l"]
}

final formula = []

// Each node is associated with at least one level
final subFormula1 = nodeIds.collect { nodeId ->
    levels.collect { l -> getVarForNodeIdAndLevel(nodeId, l) }
}
formula.addAll(subFormula1)

// Each node is associated with at most one level
final subFormula2 = [nodeIds, levels].combinations()
        .collectMany { nodeId, l ->
    final v1 = getVarForNodeIdAndLevel(nodeId, l)
    levels.findAll { it > l }.collect { k ->
        [-v1, -getVarForNodeIdAndLevel(nodeId, k)]
    }
}
formula.addAll(subFormula2)

// If level l < |N| is empty (i.e., does not contain any node),
// then level l + 1 is empty
final subFormula3 = levels.findAll { it < numLevels }.collectMany { l ->
    final ante = nodeIds.collect { nodeId ->
        getVarForNodeIdAndLevel(nodeId, l)
    }
    final lPlus1 = l + 1
    nodeIds.collect { nodeId ->
        ante + -getVarForNodeIdAndLevel(nodeId, lPlus1)
    }
}
formula.addAll(subFormula3)

// If level l > 1 is not empty, then level l - 1 is not empty
final subFormula4 = levels.findAll { it > 1 }.collectMany { l ->
    final lMinus1 = l - 1
    final cons = nodeIds.collect { nodeId ->
        getVarForNodeIdAndLevel(nodeId, lMinus1)
    }
    nodeIds.collect { nodeId ->
        [-getVarForNodeIdAndLevel(nodeId, l)] + cons
    }
}
formula.addAll(subFormula4)

// For every edge (m, n), if m occurs at level l,
// then n cannot occur at level k > l + 1
final node2id = id2node.inject([:]) { acc, k, v -> acc[v] = k ; acc}
final subFormula5 = rawEdges.collectMany { m, n ->
    final mId = node2id[m]
    final nId = node2id[n]
    levels.collectMany { l ->
        final v1 = getVarForNodeIdAndLevel(mId, l)
        levels.findAll { it > l + 1 }.collect { k ->
            [-v1, -getVarForNodeIdAndLevel(nId, k)]
        }
    }
}
formula.addAll(subFormula5)

// If node m and n occur at level l, then
// there exists two edges (p, m) and (q, n) such that
// p and q occur at level l - 1
def combinations(list) {
    list.any { it.empty } ? [] : list.combinations()
}

final edges = rawEdges.collect { e -> e.collect(node2id.&get) }
final sortedNodesIds = nodeIds.sort()
final subFormula6 = [sortedNodesIds, sortedNodesIds, levels].combinations()
        .findAll { it[0] != it[1] }.collectMany { m, n, l ->
    final vM = getVarForNodeIdAndLevel(m, l)
    final vN = getVarForNodeIdAndLevel(n, l)
    final mEdges = edges.findAll { it[1] == m }
    final nEdges = edges.findAll { it[1] == n }
    final lMinus1 = l - 1
    if (lMinus1) {
        final pqs = combinations([mEdges, nEdges])
                .collect { [it[0][0], it[1][0]] }
        final clause1 = [[-vM, -vN] + pqs.collect { p, q ->
            getVarForNodeIdPairAndLevel(p, q, lMinus1)
        }]
        final clause2 = pqs.collectMany { p, q ->
            final tmp1 = getVarForNodeIdPairAndLevel(p, q, lMinus1)
            final tmp2 = getVarForNodeIdAndLevel(p, lMinus1)
            final tmp3 = getVarForNodeIdAndLevel(q, lMinus1)
            [[-tmp1, tmp2], [-tmp1, tmp3], [-tmp2, -tmp3, tmp1]]
        }
        clause1 + clause2
    } else
        [[-vM, -vN]]
}
formula.addAll(subFormula6)

// Level 1 has at least one node
formula.add(nodeIds.collect { getVarForNodeIdAndLevel(it, 1) })

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

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

file1.withPrintWriter { writer ->
    final tmp1 = formula.unique { it.sort().join() }
    writer.println "p cnf ${varMap.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 level2nodes = [:].withDefault { [] }
final var2nodeIdLevel = nodeIdLevel2var.collectEntries { k, v -> [v, k] }
output1[1].split(' ').collect { it as int }.findAll { it in var2nodeIdLevel }
        .each {
    final tmp2 = var2nodeIdLevel[it].split(',')
    final node = id2node[tmp2[0][1..-1] as int]
    final level = tmp2[1][1..-1] as int
    level2nodes[level] << node
}

println "Node,Level"
level2nodes.sort { it.getKey() }.each { l, nodes ->
    nodes.each { n -> println "$n,$l" }
}

println ""
println "Node,Pos"
def pos = 1
(1..level2nodes.size()).each { l ->
    level2nodes[l].each { n ->
        println "$n,$pos"
        pos++
    }
}