MINCE - Global Variable Ordering for SAT & BDDs

MINCE (Min-cut vertex/variable reorderings)

A new static global variable ordering for SAT & BDDs

MINCE 0.1 is now available!!

Introduction

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

CAPO: http://vlsicad.cs.ucla.edu/software/PDtools/

GRASP: http://nexus6.cs.ucla.edu/GSRC/bookshelf/Slots/SAT/GRASP/

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.