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...

Macros
#define	DD_BIGGY 100000000

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

Typedefs
typedef struct cuddPathPair	cuddPathPair
	Type of item stored in memoization table.

Functions
DdNode *	Cudd_Eval (DdManager dd, DdNode f, int *inputs)
	Returns the value of a DD for a given variable assignment. More...

DdNode *	Cudd_ShortestPath (DdManager manager, DdNode f, int weight, int support, int *length)
	Finds a shortest path in a DD. More...

DdNode *	Cudd_LargestCube (DdManager manager, DdNode f, int *length)
	Finds a largest cube in a DD. More...

int	Cudd_ShortestLength (DdManager manager, DdNode f, int *weight)
	Find the length of the shortest path(s) in a DD. More...

DdNode *	Cudd_Decreasing (DdManager dd, DdNode f, int i)
	Checks whether a BDD is negative unate in a variable. More...

DdNode *	Cudd_Increasing (DdManager dd, DdNode f, int i)
	Checks whether a BDD is positive unate in a variable. More...

int	Cudd_EquivDC (DdManager dd, DdNode F, DdNode G, DdNode D)
	Tells whether F and G are identical wherever D is 0. More...

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. More...

int	Cudd_EqualSupNorm (DdManager dd, DdNode f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr)
	Compares two ADDs for equality within tolerance. More...

DdNode *	Cudd_bddMakePrime (DdManager dd, DdNode cube, DdNode *f)
	Expands cube to a prime implicant of f. More...

DdNode *	Cudd_bddMaximallyExpand (DdManager dd, DdNode lb, DdNode ub, DdNode f)
	Expands lb to prime implicants of (f and ub). More...

DdNode *	Cudd_bddLargestPrimeUnate (DdManager dd, DdNode f, DdNode *phaseBdd)
	Find a largest prime implicant of a unate function. More...

DdNode *	cuddBddMakePrime (DdManager dd, DdNode cube, DdNode *f)
	Performs the recursive step of Cudd_bddMakePrime. More...

static enum st_retval	freePathPair (void key, void value, void *arg)
	Frees the entries of the visited symbol table. More...

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. More...

static DdNode *	getPath (DdManager manager, st_table visited, DdNode f, int weight, int cost)
	Build a BDD for a shortest path of f. More...

static cuddPathPair	getLargest (DdManager dd, DdNode root, st_table *visited)
	Finds the size of the largest cube(s) in a DD. More...

static DdNode *	getCube (DdManager manager, st_table visited, DdNode *f, int cost)
	Build a BDD for a largest cube of f. More...

static DdNode *	ddBddMaximallyExpand (DdManager dd, DdNode lb, DdNode ub, DdNode f)
	Performs the recursive step of Cudd_bddMaximallyExpand. More...

static int	ddBddShortestPathUnate (DdManager dd, DdNode f, int phases, st_table table)
	Performs shortest path computation on a unate function. More...

static DdNode *	ddGetLargestCubeUnate (DdManager dd, DdNode f, int phases, st_table table)
	Extracts largest prime of a unate function. More...

Detailed Description

Functions for the solution of satisfiability related problems.

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

◆ Cudd_bddLargestPrimeUnate()

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

◆ Cudd_bddLeqUnless()

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

◆ Cudd_bddMakePrime()

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

◆ Cudd_bddMaximallyExpand()

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

◆ Cudd_Decreasing()

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

◆ Cudd_EqualSupNorm()

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

◆ Cudd_EquivDC()

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

◆ Cudd_Eval()

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

◆ Cudd_Increasing()

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

◆ Cudd_LargestCube()

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

◆ Cudd_ShortestLength()

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

◆ 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

◆ cuddBddMakePrime()

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

◆ ddBddMaximallyExpand()

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

◆ ddBddShortestPathUnate()

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

◆ ddGetLargestCubeUnate()

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

◆ freePathPair()

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

◆ getCube()

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

◆ getLargest()

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

◆ getPath()

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

◆ getShortest()

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.

Data Structures

Macros

Typedefs

Functions

Detailed Description

Function Documentation

◆ Cudd_bddLargestPrimeUnate()

◆ Cudd_bddLeqUnless()

◆ Cudd_bddMakePrime()

◆ Cudd_bddMaximallyExpand()

◆ Cudd_Decreasing()

◆ Cudd_EqualSupNorm()

◆ Cudd_EquivDC()

◆ Cudd_Eval()

◆ Cudd_Increasing()

◆ Cudd_LargestCube()

◆ Cudd_ShortestLength()

◆ Cudd_ShortestPath()

◆ cuddBddMakePrime()

◆ ddBddMaximallyExpand()

◆ ddBddShortestPathUnate()

◆ ddGetLargestCubeUnate()

◆ freePathPair()

◆ getCube()

◆ getLargest()

◆ getPath()

◆ getShortest()