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

** **

** **

**Executables**

- MINCE, version 0.1, download
the tarred, gzipped executable

Intel/Linux - [Mince_Linux_v01.tar.gz] (1.6 Mb)

Sun/Solaris - [Mince_Solaris_v01.tar.gz] (1.7 Mb)

**Other**

** **

**References**

** **

- F. Aloul, I. Markov, and K. Sakallah, "
**MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation,**" in Journal of Universal Computer Science (JUCS), 10(12), pp. 1562-1596, Dec. 2004. [pdf]

- F. Aloul, I. Markov, and K. Sakallah, "
**Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering,**" in Proc. of the International Conference on Computer Design (ICCD), 2002. [pdf]

- F. Aloul, I. Markov, and
K. Sakallah, "
**Faster SAT and Smaller BDDs via Common Function Structure**," in Proc. of the International Conference on Computer Aided Design (ICCAD), 2001. [pdf]

- F. Aloul, I. Markov, and
K. Sakallah, "
**MINCE: A Static Global Variable-Ordering for SAT and BDD**," in the International Workshop on Logic & Synthesis (IWLS), 2001. [pdf] [slides]

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