SddManager

class pysdd.sdd.SddManager(long var_count=1, bool auto_gc_and_minimize=False, Vtree vtree=None)

Creates a new SDD manager, either given a vtree or using a balanced vtree over the given number of variables.

Parameters:

• var_count – Number of variables
• auto_gc_and_minimize – Automatic garbage collection Automatic garbage collection and automatic SDD minimization are activated in the created manager when auto gc and minimize is not 0.
• vtree – The manager copies the input vtree. Any manipulations performed by the manager are done on its own copy, and does not affect the input vtree.

The creation and manipulation of SDDs are maintained by an SDD manager. The use of an SDD manager is analogous to the use of managers in OBDD packages such as CUDD [10]. For a discussion on the design and implementation of such systems, see [7].

To declare an SDD manager, one provides an initial vtree. By declaring an initial vtree, we also declare an initial number of variables. See the section on creating vtrees, for a few ways to specify an initial vtree.

Note that variables are referred to by an index. If there are n variables in an SDD manager, then the variables are referred to as 1, … , n. Literals are referred to by signed indices. For example, given the i-th variable, we refer to its positive literal by i and its negative literal by −i.

add_var_after(self, SddLiteral target_var)

Let v be the vtree leaf node labeled with variable target var. A new leaf node labeled with variable n + 1 is created and made a right sibling of leaf v.

add_var_after_last(self)

Let v be the rightmost leaf node in the vtree. A new leaf node labeled with variable n + 1 is created and made a right sibling of leaf v.

add_var_before(self, SddLiteral target_var)

Let v be the vtree leaf node labeled with variable target var. A new leaf node labeled with variable n + 1 is created and made a left sibling of leaf v.

add_var_before_first(self)

Let v be the leftmost leaf node in the vtree. A new leaf node labeled with variable n + 1 is created and made a left sibling of leaf v.

apply(self, SddNode node1, SddNode node2, BoolOp op)

Returns the result of combining two SDDs, where op can be CONJOIN (0) or DISJOIN (1).

auto_gc_and_minimize_off(self)

Deactivates automatic garbage collection and automatic SDD minimization.

auto_gc_and_minimize_on(self)

Activates automatic garbage collection and automatic SDD minimization.

condition(self, lit, SddNode node)

Returns the result of conditioning an SDD on a literal, where a literal is a positive or negative integer.

conjoin(self, SddNode node1, SddNode node2)

Returns the result of applying the corresponding Boolean operation on the given SDDs.

copy(self, nodes)

Returns a new SDDManager, while copying the vtree and the SDD nodes of this manager. After this operation, the given list of nodes will contain the corresponding nodes in the new manager. :param nodes: A list of SddNodes to copy. :return: The new SDDManager

count(self)

Returns the node count of all SDD nodes in the manager.

dead_count(self)

Returns the node count of all dead SDD nodes in the manager.

dead_size(self)

Returns the size of all dead SDD nodes in the manager.

disjoin(self, SddNode node1, SddNode node2)

Returns the result of applying the corresponding Boolean operation on the given SDDs.

dot(self, SddNode node=None)

SDD for the given node, formatted for use with Graphviz dot.

dot_shared(self)

Shared SDD, formatted for use with Graphviz dot.

exists(self, SddLiteral var, SddNode node)

Returns the result of existentially (universally) quantifying out a variable from an SDD.

exists_multiple(self, int[:] exists_map, SddNode node)

Returns the result of existentially quantifying out a set of variables from an SDD.

This function is expected to be more efficient than existentially quantifying out variables one at a time. The array exists map specifies the variables to be existentially quantified out. The length of exists map is expected to be n + 1, where n is the number of variables in the manager. exists map[i] should be 1 if variable i is to be quantified out; otherwise, exists map[i] should be 0. exists map[0] is unused.

exists_multiple_static(self, int[:] exists_map, SddNode node)

This is the same as sdd exists multiple, except that SDD minimization is never performed when quantifying out variables.

This can be more efficient than deactivating automatic SDD minimization and calling sdd exists multiple.

A model of an SDD is a truth assignment of the SDD variables which also satisfies the SDD. The cardinality of a truth assignment is the number of variables assigned the value true. An SDD may not mention all variables in the SDD manager. An SDD model can be converted into a global model by including the missing variables, while setting their values arbitrarily.

false(self)

Returns an SDD representing the function false.

fnf_to_sdd(self, Fnf fnf)

forall(self, SddLiteral var, SddNode node)

Returns the result of existentially (universally) quantifying out a variable from an SDD.

static from_cnf_file(char *filename, char *vtree_type='balanced')

Create an SDD from the given CNF file.

static from_cnf_string(cnf, char *vtree_type='balanced')

Create an SDD from the given CNF string.

static from_dnf_file(char *filename, char *vtree_type='balanced')

Create an SDD from the given DNF file.

static from_dnf_string(dnf, char *vtree_type='balanced')

Create an SDD from the given DNF string.

static from_fnf(Fnf fnf, char *vtree_type='balanced')

Create an SDD from the given DNF file.

static from_vtree(Vtree vtree)

Creates a new SDD manager, given a vtree.

The manager copies the input vtree. Any manipulations performed by the manager are done on its own copy, and does not affect the input vtree.

garbage_collect(self)

Performs a global garbage collection: Claims all dead SDD nodes in the manager.

get_vars(self, value)

global_minimize_cardinality(self, SddNode node)

Returns the SDD whose models are the minimum-cardinality global models of the given SDD (i.e., with respect to the manager variables).

global_model_count(self, SddNode node)

Returns the global model count of an SDD (i.e., with respect to the manager variables).

init_vtree_size_limit(self, Vtree vtree)

is_auto_gc_and_minimize_on(self)

Is automatic garbage collection and automatic SDD minimization activated?

is_prevent_transformation_on(self)

Are transformations prevented when self.is_auto_gc_and_minimize_on()=True?

is_var_used(self, var)

Returns 1 if var is referenced by a decision SDD node (dead or alive); returns 0 otherwise.

Parameters:var – Literal (number)

l(self, lit)

Short for literal(lit)

lca_of_literals(self, SddLiteral[:] literals)

Returns the smallest vtree which contains the variables of literals, where count is the number of literals.

If we view the variable of each literal as a leaf vtree node, the function will then return the lowest common ancestor (lca) of these leaf nodes.

literal(self, lit)

Returns an SDD representing a literal.

Returns an SDD representing a literal. The variable literal is of the form ±i, where i is an index of a variable, which ranges from 1 to the number of variables in the manager. If literal is positive, then the SDD representing the positive literal of the i-th variable is returned. If literal is negative, then the SDD representing the negative literal is returned.

Parameters:lit – Literal (integer number)

live_count(self)

Returns the node count of all live SDD nodes in the manager.

live_size(self)

Returns the size of all live SDD nodes in the manager.

minimize(self)

Performs global garbage collection and then tries to minimize the size of a manager’s SDD.

This function calls sdd vtree search on the manager’s vtree.

To allow for a timeout, this function can be interrupted by the keyboard interrupt (SIGINT).

minimize_cardinality(self, SddNode node)

Returns the SDD whose models are the minimum-cardinality models of the given SDD (i.e. with respect to the SDD variables).

minimize_limited(self)

minimum_cardinality(self, SddNode node)

Returns the minimum-cardinality of an SDD.

The smallest cardinality attained by any of its models. The minimum-cardinality of an SDD is the same whether or not we consider the global models of the SDD.

model_count(self, SddNode node)

Returns the model count of an SDD (i.e., with respect to the SDD variables).

negate(self, SddNode node)

Returns the result of applying the corresponding Boolean operation on the given SDDs.

print_stdout(self)

read_cnf_file(self, filename)

Replace the SDD by an SDD representing the theory in the given CNF file.

read_dnf_file(self, filename)

Replace the SDD by an SDD representing the theory in the given DNF file.

read_sdd_file(self, char *filename)

Reads an SDD from file.

The read SDD is guaranteed to be equivalent to the one in the file, but may have a different structure depending on the current vtree of the manager. SDD minimization will not be performed when reading an SDD from file, even if auto SDD minimization is active.

rename_variables(self, SddNode node, SddLiteral[:] variable_map)

Returns an SDD which is obtained by renaming variables in the SDD node. The array variable_map has size n+1, where n is the number of variables in the manager. A variable i, 1 <= i <= n, that appears in the given SDD is renamed into variable variable_map[i] (variable_map[0] is not used).

root

root: object

save(self, char *filename, SddNode node)

Saves an SDD to file.

Typically, one also saves the corresponding vtree to file. This allows one to read the SDD back using the same vtree.

save_as_dot(self, char *filename, SddNode node)

Saves an SDD to file, formatted for use with Graphviz dot.

set_options(self, options=None)

set_prevent_transformation(self, prevent=True)

Prevent transformations when prevent=True and self.is_auto_gc_and_minimize_on()=True

set_vtree_apply_time_limit(self, float time_limit)

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

set_vtree_cartesian_product_limit(self, SddSize size_limit)

Sets the absolute size limit on the size of a cartesian product for right rotation and swap operations.

Default value is 8, 192.

set_vtree_fragment_time_limit(self, float time_limit)

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

set_vtree_operation_memory_limit(self, float memory_limit)

Sets the relative memory limit for rotation and swap operations. Default value is 3.0.

set_vtree_operation_size_limit(self, float size_limit)

Sets the relative size limit for rotation and swap operations.

Default value is 1.2. A size limit l is relative to the size s of an SDD for a given vtree (s is called the reference size). Hence, using this size limit requires calling the following functions to set and update the reference size s, otherwise the behavior is not defined.

set_vtree_operation_time_limit(self, float time_limit)

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

set_vtree_search_convergence_threshold(self, float threshold)

set_vtree_search_time_limit(self, float time_limit)

Set the time limits for the vtree search algorithm.

A vtree operation is either a rotation or a swap. Times are in seconds and correspond to CPU time. Default values, in order, are 180, 60, 30, and 10 seconds.

shared_save_as_dot(self, char *filename)

Saves the SDD of the manager’s vtree (a shared SDD), formatted for use with Graphviz dot.

size(self)

Returns the size of all SDD nodes in the manager.

true(self)

Returns an SDD representing the function true.

update_vtree_size_limit(self)

var_count(self)

Returns the number of SDD variables currently associated with the manager.

var_order(self)

Return an array var order (whose length will be equal the number of variables in the manager) with the left-to-right variable ordering of the manager’s vtree.

vtree(self)

vtree_copy(self)

vtree_minimize(self, Vtree vtree)

Performs local garbage collection on vtree and then tries to minimize the size of the SDD of vtree by searching for a different vtree. Returns the root of the resulting vtree.

vtree_of_var(self, SddLiteral var)

Returns the leaf node of a manager’s vtree, which is associated with var.