def kColoringSAT(g: Graph, k: Int): Option[Map[Int,Int]] = {
    // Imports needed to use the SAT4J
    import org.sat4j.minisat.SolverFactory
    import org.sat4j.core.VecInt

    require(g != null && g.nofVertices > 0)
    require(k >= 1 & k <= 64)
    val N = g.nofVertices

    // Handle special cases separately
    if(k == 0) {
      if(g.nofVertices == 0) return Some(Map[Int,Int]())
      else return None
    }
    if(k == 1) {
      if((0 until N).forall(v => g.neighbours(v).isEmpty))
        return Some((0 until N).map({case v => (v,0)}).toMap)
      return None
    }

    def vertexColorToVar(vertex: Int, color: Int): Int = {
      require(0 <= vertex && vertex < N)
      require(0 <= color && color < k)
      1 + vertex + color
    }

    // Create the SAT solver instance
    val solver = SolverFactory.newDefault()
    // Tell the solver how many Boolean variables there will be
    solver.newVar(N*k)

    // Create the instance, call the SAT solver and interpret the result

    for(vertex <- 0 until N) {
      //The vertex has at least one color
      val clause = (0 until k).map(vertexColorToVar(vertex,_)).toArray
      solver.addClause(new VecInt(clause))

      //The vertex has at most one color
      for(c1 <- 0 until k) {
        for(c2 <- 0 until k) {
          val clause = Array[Int](-vertexColorToVar(vertex, c1),
                                  -vertexColorToVar(vertex, c2))
          solver.addClause(new VecInt(clause))
        }
      }

      //The nodes for every edge has different colors.
      for(c <- 0 until k) {
        for(n <- g.neighbours(vertex)) {
          val clause = Array[Int](-vertexColorToVar(vertex, c),
                                  -vertexColorToVar(n, c))
          solver.addClause(new VecInt(clause))
        }
      }
    }


    if(solver.isSatisfiable()) {
      var result = HashMap[Int, Int]()
      for(v <- 0 until N; c <- 0 until k) {
        if(solver.model(vertexColorToVar(v, c))) {
          result += ((v, c))
        }
      }
      Some(result.toMap)
    } else None



  }