Functions for exact variable reordering. More...

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddExact.c:

Functions
int	cuddExact (DdManager *table, int lower, int upper)
	Exact variable ordering algorithm. More...

static int	getMaxBinomial (int n)
	Returns the maximum value of `(n choose k)` for a given `n`. More...

static DdHalfWord **	getMatrix (int rows, int cols)
	Allocates a two-dimensional matrix of ints. More...

static void	freeMatrix (DdHalfWord **matrix)
	Frees a two-dimensional matrix allocated by getMatrix. More...

static int	getLevelKeys (DdManager *table, int l)
	Returns the number of nodes at one level of a unique table. More...

static int	ddShuffle (DdManager table, DdHalfWord permutation, int lower, int upper)
	Reorders variables according to a given permutation. More...

static int	ddSiftUp (DdManager *table, int x, int xLow)
	Moves one variable up. More...

static int	updateUB (DdManager table, int oldBound, DdHalfWord bestOrder, int lower, int upper)
	Updates the upper bound and saves the best order seen so far. More...

static int	ddCountRoots (DdManager *table, int lower, int upper)
	Counts the number of roots. More...

static void	ddClearGlobal (DdManager *table, int lower, int maxlevel)
	Scans the DD and clears the LSB of the next pointers. More...

static int	computeLB (DdManager table, DdHalfWord order, int roots, int cost, int lower, int upper, int level)
	Computes a lower bound on the size of a BDD. More...

static int	updateEntry (DdManager table, DdHalfWord order, int level, int cost, DdHalfWord *orders, int costs, int subsets, char *mask, int lower, int upper)
	Updates entry for a subset. More...

static void	pushDown (DdHalfWord *order, int j, int level)
	Pushes a variable in the order down to position "level.". More...

static DdHalfWord *	initSymmInfo (DdManager *table, int lower, int upper)
	Gathers symmetry information. More...

static int	checkSymmInfo (DdManager table, DdHalfWord symmInfo, int index, int level)
	Check symmetry condition. More...

Detailed Description

Functions for exact variable reordering.

Author: Cheng Hua, Fabio Somenzi

Copyright

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Function Documentation

◆ checkSymmInfo()

static int checkSymmInfo	(	DdManager *	table,
		DdHalfWord *	symmInfo,
		int	index,
		int	level
	)

static

Check symmetry condition.

Returns 1 if a variable is the one with the highest index among those belonging to a symmetry group that are in the top part of the BDD. The top part is given by level.

Side effects None

See also: initSymmInfo

◆ computeLB()

static int computeLB	(	DdManager *	table,
		DdHalfWord *	order,
		int	roots,
		int	cost,
		int	lower,
		int	upper,
		int	level
	)

static

Computes a lower bound on the size of a BDD.

The lower bound depends on the following factors:

size of the lower part of it;
size of the part of the upper part not subjected to reordering;
number of roots in the part of the BDD subjected to reordering;
variable in the support of the roots in the upper part of the BDD subjected to reordering.

Side effects None

Parameters

table	manager
order	optimal order for the subset
roots	roots between lower and upper
cost	minimum cost for the subset
lower	lower level to be reordered
upper	upper level to be reordered
level	offset for the current top bottom var

◆ cuddExact()

int cuddExact	(	DdManager *	table,
		int	lower,
		int	upper
	)

Exact variable ordering algorithm.

Finds an optimum order for the variables between lower and upper.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ ddClearGlobal()

static void ddClearGlobal	(	DdManager *	table,
		int	lower,
		int	maxlevel
	)

static

Scans the DD and clears the LSB of the next pointers.

The LSB of the next pointers are used as markers to tell whether a node was reached. Once the roots are counted, these flags are reset.

Side effects None

See also: ddCountRoots

◆ ddCountRoots()

static int ddCountRoots	(	DdManager *	table,
		int	lower,
		int	upper
	)

static

Counts the number of roots.

Counts the number of roots at the levels between lower and upper. The computation is based on breadth-first search. A node is a root if it is not reachable from any previously visited node. (All the nodes at level lower are therefore considered roots.) The roots that are constant nodes are always ignored. The visited flag uses the LSB of the next pointer.

Returns: the root count.

Side effects None

See also: ddClearGlobal

◆ ddShuffle()

static int ddShuffle	(	DdManager *	table,
		DdHalfWord *	permutation,
		int	lower,
		int	upper
	)

static

Reorders variables according to a given permutation.

The i-th permutation array contains the index of the variable that should be brought to the i-th level. ddShuffle assumes that no dead nodes are present and that the interaction matrix is properly initialized. The reordering is achieved by a series of upward sifts.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ ddSiftUp()

static int ddSiftUp	(	DdManager *	table,
		int	x,
		int	xLow
	)

static

Moves one variable up.

Takes a variable from position x and sifts it up to position xLow; xLow should be less than or equal to x.

Returns: 1 if successful; 0 otherwise

Side effects None

◆ freeMatrix()

static void freeMatrix ( DdHalfWord ** matrix )

static

Frees a two-dimensional matrix allocated by getMatrix.

Side effects None

See also: getMatrix

◆ getLevelKeys()

static int getLevelKeys	(	DdManager *	table,
		int	l
	)

static

Returns the number of nodes at one level of a unique table.

The projection function, if isolated, is not counted.

Side effects None

◆ getMatrix()

static DdHalfWord** getMatrix	(	int	rows,
		int	cols
	)

static

Allocates a two-dimensional matrix of ints.

Returns: the pointer to the matrix if successful; NULL otherwise.

Side effects None

See also: freeMatrix

◆ getMaxBinomial()

static int getMaxBinomial ( int n )

static

Returns the maximum value of (n choose k) for a given n.

Computes the maximum value of (n choose k) for a given n. The maximum value occurs for k = n/2 when n is even, or k = (n-1)/2 when n is odd. The algorithm used in this procedure avoids intermediate overflow problems. It is based on the identity

binomial(n,k) = n/k * binomial(n-1,k-1).

Returns: the computed value if successful; -1 if out of range.

Side effects None

◆ initSymmInfo()

static DdHalfWord* initSymmInfo	(	DdManager *	table,
		int	lower,
		int	upper
	)

static

Gathers symmetry information.

Translates the symmetry information stored in the next field of each subtable from level to indices. This procedure is called immediately after symmetric sifting, so that the next fields are correct. By translating this informaton in terms of indices, we make it independent of subsequent reorderings. The format used is that of the next fields: a circular list where each variable points to the next variable in the same symmetry group. Only the entries between lower and upper are considered. The procedure returns a pointer to an array holding the symmetry information if successful; NULL otherwise.

Side effects None

See also: checkSymmInfo

◆ pushDown()

static void pushDown	(	DdHalfWord *	order,
		int	j,
		int	level
	)

static

Pushes a variable in the order down to position "level.".

Side effects None

◆ updateEntry()

static int updateEntry	(	DdManager *	table,
		DdHalfWord *	order,
		int	level,
		int	cost,
		DdHalfWord **	orders,
		int *	costs,
		int	subsets,
		char *	mask,
		int	lower,
		int	upper
	)

static

Updates entry for a subset.

Finds the subset, if it exists. If the new order for the subset has lower cost, or if the subset did not exist, it stores the new order and cost.

Returns: the number of subsets currently in the table.

Side effects None

◆ updateUB()

static int updateUB	(	DdManager *	table,
		int	oldBound,
		DdHalfWord *	bestOrder,
		int	lower,
		int	upper
	)

static

Updates the upper bound and saves the best order seen so far.

Returns: the current value of the upper bound.

Side effects None