Functions for exact variable reordering. More...
#include "util.h"
#include "cuddInt.h"
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 DdHalfWord * | initSymmInfo (DdManager *table, int lower, int upper) |
Gathers symmetry information. | |
static int | checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level) |
Check symmetry condition. |
Functions for exact variable reordering.
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.
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.
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:
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.
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.
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.
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.
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.
static void freeMatrix | ( | DdHalfWord ** | matrix | ) | [static] |
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.
static DdHalfWord** getMatrix | ( | int | rows, | |
int | cols | |||
) | [static] |
Allocates a two-dimensional matrix of ints.
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).
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.
static void pushDown | ( | DdHalfWord * | order, | |
int | j, | |||
int | level | |||
) | [static] |
Pushes a variable in the order down to position "level.".
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.
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.