cudd/cuddSat.c File Reference

Functions for the solution of satisfiability related problems. More...

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddSat.c:

Data Structures

struct  cuddPathPair
 Type of item stored in memoization table. More...

Defines

#define DD_BIGGY   100000000
#define WEIGHT(weight, col)   ((weight) == NULL ? 1 : weight[col])

Functions

DdNodeCudd_Eval (DdManager *dd, DdNode *f, int *inputs)
 Returns the value of a DD for a given variable assignment.
DdNodeCudd_ShortestPath (DdManager *manager, DdNode *f, int *weight, int *support, int *length)
 Finds a shortest path in a DD.
DdNodeCudd_LargestCube (DdManager *manager, DdNode *f, int *length)
 Finds a largest cube in a DD.
int Cudd_ShortestLength (DdManager *manager, DdNode *f, int *weight)
 Find the length of the shortest path(s) in a DD.
DdNodeCudd_Decreasing (DdManager *dd, DdNode *f, int i)
 Checks whether a BDD is negative unate in a variable.
DdNodeCudd_Increasing (DdManager *dd, DdNode *f, int i)
 Checks whether a BDD is positive unate in a variable.
int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D)
 Tells whether F and G are identical wherever D is 0.
int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D)
 Tells whether f is less than of equal to G unless D is 1.
int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr)
 Compares two ADDs for equality within tolerance.
DdNodeCudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f)
 Expands cube to a prime implicant of f.
DdNodeCudd_bddMaximallyExpand (DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f)
 Expands lb to prime implicants of (f and ub).
DdNodeCudd_bddLargestPrimeUnate (DdManager *dd, DdNode *f, DdNode *phaseBdd)
 Find a largest prime implicant of a unate function.
DdNodecuddBddMakePrime (DdManager *dd, DdNode *cube, DdNode *f)
 Performs the recursive step of Cudd_bddMakePrime.
static enum st_retval freePathPair (void *key, void *value, void *arg)
 Frees the entries of the visited symbol table.
static cuddPathPair getShortest (DdManager *dd, DdNode *root, int *cost, int *support, st_table *visited)
 Finds the length of the shortest path(s) in a DD.
static DdNodegetPath (DdManager *manager, st_table *visited, DdNode *f, int *weight, int cost)
 Build a BDD for a shortest path of f.
static cuddPathPair getLargest (DdManager *dd, DdNode *root, st_table *visited)
 Finds the size of the largest cube(s) in a DD.
static DdNodegetCube (DdManager *manager, st_table *visited, DdNode *f, int cost)
 Build a BDD for a largest cube of f.
static DdNodeddBddMaximallyExpand (DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f)
 Performs the recursive step of Cudd_bddMaximallyExpand.
static int ddBddShortestPathUnate (DdManager *dd, DdNode *f, int *phases, st_table *table)
 Performs shortest path computation on a unate function.
static DdNodeddGetLargestCubeUnate (DdManager *dd, DdNode *f, int *phases, st_table *table)
 Extracts largest prime of a unate function.

Detailed Description

Functions for the solution of satisfiability related problems.

Author:
Seh-Woong Jeong, 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

DdNode* Cudd_bddLargestPrimeUnate ( DdManager dd,
DdNode f,
DdNode phaseBdd 
)

Find a largest prime implicant of a unate function.

The behavior is undefined if f is not unate. The third argument is used to determine whether f is unate positive (increasing) or negative (decreasing) in each of the variables in its support.

Returns:
the BDD for the prime if succesful; NULL otherwise.
Side effects
None
See also:
Cudd_bddMaximallyExpand
Parameters:
dd manager
f unate function
phaseBdd cube of the phases
int Cudd_bddLeqUnless ( DdManager dd,
DdNode f,
DdNode g,
DdNode D 
)

Tells whether f is less than of equal to G unless D is 1.

f, g, and D are BDDs. No new nodes are created.

Returns:
1 if f is less than of equal to G, and 0 otherwise.
Side effects
None
See also:
Cudd_EquivDC Cudd_bddLeq Cudd_bddIteConstant
DdNode* Cudd_bddMakePrime ( DdManager dd,
DdNode cube,
DdNode f 
)

Expands cube to a prime implicant of f.

Returns:
the prime if successful; NULL otherwise. In particular, NULL is returned if cube is not a real cube or is not an implicant of f.
Side effects
None
See also:
Cudd_bddMaximallyExpand
Parameters:
dd manager
cube cube to be expanded
f function of which the cube is to be made a prime
DdNode* Cudd_bddMaximallyExpand ( DdManager dd,
DdNode lb,
DdNode ub,
DdNode f 
)

Expands lb to prime implicants of (f and ub).

Expands lb to all prime implicants of (f and ub) that contain lb. Assumes that lb is contained in ub.

Returns:
the disjunction of the primes if lb is contained in f; returns the zero BDD if lb is not contained in f; returns NULL in case of failure. In particular, NULL is returned if cube is not a real cube or is not an implicant of f. Returning the disjunction of all prime implicants works because the resulting function is unate.
Side effects
None
See also:
Cudd_bddMakePrime
Parameters:
dd manager
lb cube to be expanded
ub upper bound cube
f function against which to expand
DdNode* Cudd_Decreasing ( DdManager dd,
DdNode f,
int  i 
)

Checks whether a BDD is negative unate in a variable.

Determines whether the function represented by BDD f is negative unate (monotonic decreasing) in variable i. This function does not generate any new nodes.

Returns:
the constant one is f is unate and the (logical) constant zero if it is not.
Side effects
None
See also:
Cudd_Increasing
int Cudd_EqualSupNorm ( DdManager dd,
DdNode f,
DdNode g,
CUDD_VALUE_TYPE  tolerance,
int  pr 
)

Compares two ADDs for equality within tolerance.

Two ADDs are reported to be equal if the maximum difference between them (the sup norm of their difference) is less than or equal to the tolerance parameter. If parameter pr is positive the first failure is reported to the standard output.

Returns:
1 if the two ADDs are equal (within tolerance); 0 otherwise.
Side effects
None
Parameters:
dd manager
f first ADD
g second ADD
tolerance maximum allowed difference
pr verbosity level
int Cudd_EquivDC ( DdManager dd,
DdNode F,
DdNode G,
DdNode D 
)

Tells whether F and G are identical wherever D is 0.

F and G are either two ADDs or two BDDs. D is either a 0-1 ADD or a BDD. No new nodes are created.

Returns:
1 if F and G are equivalent, and 0 otherwise.
Side effects
None
See also:
Cudd_bddLeqUnless
DdNode* Cudd_Eval ( DdManager dd,
DdNode f,
int *  inputs 
)

Returns the value of a DD for a given variable assignment.

The variable assignment is passed in an array of int's, that should specify a zero or a one for each variable in the support of the function.

Returns:
a pointer to a constant node. No new nodes are produced.
Side effects
None
See also:
Cudd_bddLeq Cudd_addEvalConst
DdNode* Cudd_Increasing ( DdManager dd,
DdNode f,
int  i 
)

Checks whether a BDD is positive unate in a variable.

Determines whether the function represented by BDD f is positive unate (monotonic increasing) in variable i. It is based on Cudd_Decreasing and the fact that f is monotonic increasing in i if and only if its complement is monotonic decreasing in i.

Side effects
None
See also:
Cudd_Decreasing
DdNode* Cudd_LargestCube ( DdManager manager,
DdNode f,
int *  length 
)

Finds a largest cube in a DD.

f is the DD we want to get the largest cube for. The problem is translated into the one of finding a shortest path in f, when both THEN and ELSE arcs are assumed to have unit length. This yields a largest cube in the disjoint cover corresponding to the DD. Therefore, it is not necessarily the largest implicant of f.

Returns:
the largest cube as a BDD.
Side effects
The number of literals of the cube is returned in the location pointed by length if it is non-null.
See also:
Cudd_ShortestPath
int Cudd_ShortestLength ( DdManager manager,
DdNode f,
int *  weight 
)

Find the length of the shortest path(s) in a DD.

f is the DD we want to get the shortest path for; weight\[i\] is the weight of the THEN edge coming from the node whose index is i. All ELSE edges have 0 weight.

Returns:
the length of the shortest path(s) if such a path is found; a large number if the function is identically 0, and CUDD_OUT_OF_MEM in case of failure.
Side effects
None
See also:
Cudd_ShortestPath
DdNode* Cudd_ShortestPath ( DdManager manager,
DdNode f,
int *  weight,
int *  support,
int *  length 
)

Finds a shortest path in a DD.

f is the DD we want to get the shortest path for; weight\[i\] is the weight of the THEN arc coming from the node whose index is i. If weight is NULL, then unit weights are assumed for all THEN arcs. All ELSE arcs have 0 weight. If non-NULL, both weight and support should point to arrays with at least as many entries as there are variables in the manager.

Returns:
the shortest path as the BDD of a cube.
Side effects
support contains on return the true support of f. If support is NULL on entry, then Cudd_ShortestPath does not compute the true support info. length contains the length of the path.
See also:
Cudd_ShortestLength Cudd_LargestCube
DdNode* cuddBddMakePrime ( DdManager dd,
DdNode cube,
DdNode f 
)

Performs the recursive step of Cudd_bddMakePrime.

Returns:
the prime if successful; NULL otherwise.
Side effects
None
Parameters:
dd manager
cube cube to be expanded
f function of which the cube is to be made a prime
static DdNode* ddBddMaximallyExpand ( DdManager dd,
DdNode lb,
DdNode ub,
DdNode f 
) [static]

Performs the recursive step of Cudd_bddMaximallyExpand.

On entry to this function, ub and lb should be different from the zero BDD. The function then maintains this invariant.

Returns:
set of primes or zero BDD if successful; NULL otherwise.
Side effects
None

There are three major terminal cases in theory: ub -> f : return ub lb == f : return lb not(lb -> f): return zero Only the second case can be checked exactly in constant time. For the others, we check for sufficient conditions.

Parameters:
dd manager
lb cube to be expanded
ub upper bound cube
f function against which to expand
static int ddBddShortestPathUnate ( DdManager dd,
DdNode f,
int *  phases,
st_table table 
) [static]

Performs shortest path computation on a unate function.

This function is based on the observation that in the BDD of a unate function no node except the constant is reachable from the root via paths of different parity.

Returns:
the length of the shortest path to one if successful; CUDD_OUT_OF_MEM otherwise.
Side effects
None
See also:
getShortest
static DdNode* ddGetLargestCubeUnate ( DdManager dd,
DdNode f,
int *  phases,
st_table table 
) [static]

Extracts largest prime of a unate function.

Returns:
the BDD of the prime if successful; NULL otherwise.
Side effects
None
See also:
getPath
static enum st_retval freePathPair ( void *  key,
void *  value,
void *  arg 
) [static]

Frees the entries of the visited symbol table.

Returns:
ST_CONTINUE.
Side effects
None
static DdNode* getCube ( DdManager manager,
st_table visited,
DdNode f,
int  cost 
) [static]

Build a BDD for a largest cube of f.

Given the minimum length from the root, and the minimum lengths for each node (in visited), apply triangulation at each node. Of the two children of each node on a shortest path, at least one is on a shortest path. In case of ties the procedure chooses the THEN children.

Returns:
a pointer to the cube BDD representing the path if successful; NULL otherwise.
Side effects
None
static cuddPathPair getLargest ( DdManager dd,
DdNode root,
st_table visited 
) [static]

Finds the size of the largest cube(s) in a DD.

This problem is translated into finding the shortest paths from a node when both THEN and ELSE arcs have unit lengths. Uses a local symbol table to store the lengths for each node. Only the lengths for the regular nodes are entered in the table, because those for the complement nodes are simply obtained by swapping the two lenghts.

Returns:
a pair of lengths: the length of the shortest path to 1; and the length of the shortest path to 0. This is done so as to take complement arcs into account.
Side effects
none
static DdNode* getPath ( DdManager manager,
st_table visited,
DdNode f,
int *  weight,
int  cost 
) [static]

Build a BDD for a shortest path of f.

Given the minimum length from the root, and the minimum lengths for each node (in visited), apply triangulation at each node. Of the two children of each node on a shortest path, at least one is on a shortest path. In case of ties the procedure chooses the THEN children.

Returns:
a pointer to the cube BDD representing the path if successful; NULL otherwise.
Side effects
None
static cuddPathPair getShortest ( DdManager dd,
DdNode root,
int *  cost,
int *  support,
st_table visited 
) [static]

Finds the length of the shortest path(s) in a DD.

Uses a local symbol table to store the lengths for each node. Only the lengths for the regular nodes are entered in the table, because those for the complement nodes are simply obtained by swapping the two lenghts.

Returns:
a pair of lengths: the length of the shortest path to 1; and the length of the shortest path to 0. This is done so as to take complement arcs into account.
Side effects
Accumulates the support of the DD in support.
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1