MINCE (Min-cut vertex/variable reorderings)

A new static global variable ordering for SAT & BDDs



MINCE 0.1 is now available!!






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.


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).


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.)




Intel/Linux  - [Mince_Linux_v01.tar.gz]  (1.6 Mb)
Sun/Solaris - [Mince_Solaris_v01.tar.gz]  (1.7 Mb)











Maintained by Fadi Aloul(faloul@aus.edu)
Last updated February 16, 2003.