<![if !supportEmptyParas]><![endif]> 

<![if !supportEmptyParas]><![endif]> 

<![if !supportEmptyParas]><![endif]> 

Introduction

<![if !supportEmptyParas]><![endif]> 

In many applications, it is beneficial to order vertices of a graph/hypergraph such that the total (or average) length/span of edges/hyper-edges is minimized. Other related objectives are cut-width/bandwidth, total (or average) cut, etc. Recursive min-cut bisection tends to return solutions that are simultaneously good with respect to many of these objectives.

<![if !supportEmptyParas]><![endif]> 

This page offers a leading-edge generic implementation of such vertex reordering and a specific application to variable re-orderings for the Boolean Satisfiability (SAT) problem and Binary Decision Diagrams (BDDs) (the MINCE heuristic).

Example

Check out the structure of the hole7.cnf instance from the pigeon-hole family: [Original variable order] and [Mince variable order].
(Variables are represented by points on the x-axis and clauses are represented by stars of edges that connect those points.)

<![if !supportEmptyParas]><![endif]> 

<![if !supportEmptyParas]><![endif]> 

<![if !supportEmptyParas]><![endif]> 

<![if !supportEmptyParas]><![endif]> 

<![if !supportEmptyParas]><![endif]>