Generate Edge Intersection Graph

Header: fiction/algorithms/graph/generate_edge_intersection_graph.hpp

struct generate_edge_intersection_graph_params

Parameters for the edge intersection graph generation algorithm.

Public Members

bool crossings = false

Allow crossings by not creating edges between paths that only share single-coordinate sub-paths.

std::optional<uint32_t> path_limit = std::nullopt

If a value is given, for each objective, only up to the path_limit shortest paths will be enumerated (using Yen’s algorithm) instead of all paths.

struct generate_edge_intersection_graph_stats

Public Members

mockturtle::stopwatch::duration time_total = {0}

Runtime measurement.

std::size_t number_of_unroutable_objectives = {0}

For each routing objective that cannot be fulfilled in the given layout, this counter is incremented.

std::vector<std::vector<std::size_t>> cliques = {}

Stores all cliques in the resulting graph that were created during path enumeration. There might be more cliques in the overall graph but these ones correspond to one routing objective each, which could be useful information to have in certain algorithms.

std::size_t num_vertices

Stores the size of the generated edge intersection graph.

template<typename Lyt>
edge_intersection_graph<Lyt> fiction::generate_edge_intersection_graph(const Lyt &lyt, const std::vector<routing_objective<Lyt>> &objectives, generate_edge_intersection_graph_params ps = {}, generate_edge_intersection_graph_stats *pst = nullptr)

Creates an edge intersection graph of all paths that satisfy a given list of routing objectives. That is, this function generates an undirected graph whose nodes represent paths in the given layout and whose edges represent intersections of these paths. An intersection is understood as the non-disjunction of paths, i.e., they share at least one coordinate. To generate the paths for the routing objectives, all possible paths from source to target in the layout are enumerated while taking obstructions into consideration. The given layout must be clocked.

Template Parameters:

Lyt – Type of the clocked layout.

Parameters:

• lyt – The layout to generate the edge intersection graph for.

• objectives – A list of routing objectives given as source-target pairs.

• ps – Parameters.

• pst – Statistics.

Returns:

An edge intersection graph of paths satisfying the given routing objectives in lyt.

Graph Coloring

C++Python

Header: fiction/algorithms/graph/graph_coloring.hpp

enum class fiction::graph_coloring_engine

An enumeration of coloring engines to use for the graph coloring. All but SAT are using the graph-coloring library by Brian Crites.

Values:

enumerator MCS

Optimal coloring for chordal graphs proposed in “Register Allocation via Coloring of Chordal Graphs” by Jens Palsberg in CATS 2007.

enumerator DSATUR

Saturation degree algorithm proposed in “New Methods to Color the Vertices of a Graph” by Daniel Brélaz in Communications of the ACM, 1979. This algorithm is a heuristic but is exact for bipartite graphs.

enumerator LMXRLF

A randomized heuristic algorithm that combines various paradigms like divide-and-conquer, objective functions, reuse of intermediate solutions etc. It was proposed in “Efficient Coloring of a Large Spectrum of Graphs” by Darko Kirovski and Miodrag Potkonjak in DAC 1998. While this algorithm is really performant, it tends to find non-optimal solutions even for small instances.

enumerator TABUCOL

A \(k\)-coloring algorithm using tabu search proposed in “Using Tabu Search Techniques for Graph Coloring” by A. Hertz and D. de Werra in Computing 1987. The authors claim that it significantly outperforms simulated annealing. However, since it is a \(k\)-coloring algorithm, it is required to set k_color_value in determine_vertex_coloring_params to the chromatic number that is to be checked for.

enumerator SAT

Custom iterative SAT-based encoding that finds optimal colorings.

enum class fiction::graph_coloring_sat_search_tactic

An enumeration of search tactics to use for the SAT-based graph coloring to determine a min-coloring.

Values:

enumerator LINEARLY_ASCENDING

Ascend linearly by checking for \(k = 1, 2, 3, \dots\) until SAT. If at least one clique is passed, \(k\) starts at the largest clique size \(|C|\) instead with \(k = |C|, |C| + 1, |C| + 2, \dots\)

enumerator LINEARLY_DESCENDING

Descend linearly by checking for \(k = |G|, |G| - 1, |G| - 2, \dots\) until UNSAT.

enumerator BINARY_SEARCH

First ascend exponentially by checking for \(k = 2^0, 2^1, 2^2, \dots\) until SAT, then perform binary search in the window \([2^{h-1}, 2^h]\), where \(2^h\) was the first SAT. If at least one clique is passed, \(k\) starts at the largest clique size \(|C|\) instead with \(k = 2^0 \cdot |C|, 2^1 \cdot |C|, 2^2 \cdot |C|, \dots\)

template<typename Graph>
struct determine_vertex_coloring_sat_params

Parameters for SAT-based graph coloring.

Template Parameters:

Graph – Type of the graph to color.

Public Members

bill::solvers sat_engine = bill::solvers::ghack

The SAT solver to use.

graph_coloring_sat_search_tactic sat_search_tactic = graph_coloring_sat_search_tactic::LINEARLY_ASCENDING

The search tactic to apply.

std::vector<std::vector<typename Graph::vertex_id_type>> cliques = {}

If cliques in the passed graph are known, they can be used for symmetry breaking in the SAT engine which significantly speeds up runtime. The bigger the cliques, the better.

bool clique_size_color_frequency = false

Tries to establish the color frequency of color 0 such that it equals the largest clique size.

struct determine_vertex_coloring_heuristic_params

Parameters for heuristic graph coloring.

Public Members

std::size_t k_color_value = 0

\(k\)-color value for \(k\)-coloring algorithms, e.g., TABUCOL.

template<typename Graph>
struct determine_vertex_coloring_params

Common parameters for the graph coloring algorithm.

Template Parameters:

Graph – Type of the graph to color.

Public Members

graph_coloring_engine engine = graph_coloring_engine::MCS

The engine to use.

determine_vertex_coloring_sat_params<Graph> sat_params = {}

Parameters for engine == SAT.

determine_vertex_coloring_heuristic_params heuristic_params = {}

Parameters for engine != SAT.

bool verify_coloring_after_computation = false

Verify that the found coloring is valid.

template<typename Color = std::size_t>
struct determine_vertex_coloring_stats

Public Members

mockturtle::stopwatch::duration time_total = {0}

Runtime measurement.

std::size_t chromatic_number = {0}

The determined chromatic number (could be non-optimal depending on the applied engine).

Color most_frequent_color = {0}

The color that appeared the most.

std::size_t color_frequency = {0}

The frequency of the most used color.

std::optional<bool> coloring_verified = std::nullopt

Validation result of the coloring (std::nullopt = none attempted, true = valid, false = invalid).

template<typename Graph, typename Color = std::size_t>
vertex_coloring<Graph, Color> fiction::determine_vertex_coloring(const Graph &graph, determine_vertex_coloring_params<Graph> ps = {}, determine_vertex_coloring_stats<Color> *pst = nullptr)

This function provides an interface to call various vertex coloring algorithms on the given graph. A vertex coloring is the assignment of colors to graph vertices such that no two vertices that share an edge receive the same color. If a graph is colorable with \(k\) colors, the graph is said to be \(k\)-colorable. The minimum value of \(k\) for a graph is called its chromatic number. To determine the chromatic number of a graph is \(NP\)-complete in general. The provided algorithms attempt to get as close to the optimum coloring as possible. However, no heuristic can give an optimality guarantee. If the exact chromatic number is required, the SAT-based engine must be used. This may require exponential runtime in the worst case but is, on average, a lot faster due to the smart traversal of search spaces that SAT solvers provide.

See graph_coloring_engine for a list of all supported engines.

Note

If the clique_size_color_frequency parameter is set together with the SAT engine, there is no guarantee that the SAT solver is able to find a valid coloring. In that case, this algorithm falls back to MCS.

Template Parameters:

• Graph – Graph type to color.

• Color – Color type to use.

Parameters:

• graph – The graph whose vertices are to be colored.

• ps – Parameters.

• pst – Statistics.

Returns:

An assignment of graph vertices to colors such that no two adjacent vertices share the same color.