cudd/cuddExact.c File Reference

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.
static int getMaxBinomial (int n)
 Returns the maximum value of `(n choose k)` for a given `n`.
static DdHalfWord ** getMatrix (int rows, int cols)
 Allocates a two-dimensional matrix of ints.
static void freeMatrix (DdHalfWord **matrix)
 Frees a two-dimensional matrix allocated by getMatrix.
static int getLevelKeys (DdManager *table, int l)
 Returns the number of nodes at one level of a unique table.
static int ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper)
 Reorders variables according to a given permutation.
static int ddSiftUp (DdManager *table, int x, int xLow)
 Moves one variable up.
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.
static int ddCountRoots (DdManager *table, int lower, int upper)
 Counts the number of roots.
static void ddClearGlobal (DdManager *table, int lower, int maxlevel)
 Scans the DD and clears the LSB of the next pointers.
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.
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.
static void pushDown (DdHalfWord *order, int j, int level)
 Pushes a variable in the order down to position "level.".
static DdHalfWordinitSymmInfo (DdManager *table, int lower, int upper)
 Gathers symmetry information.
static int checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level)
 Check symmetry condition.

Detailed Description

Functions for exact variable reordering.

Author:
Cheng Hua, Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

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

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
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
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
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
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
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
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
static void freeMatrix ( DdHalfWord **  matrix  )  [static]

Frees a two-dimensional matrix allocated by getMatrix.

Side effects
None
See also:
getMatrix
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
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
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
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
static void pushDown ( DdHalfWord order,
int  j,
int  level 
) [static]

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

Side effects
None
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
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
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1