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

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

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_after_lca

Let v be the smallest vtree which contains the variables of literals, where count is the number of literals. A new leaf node labeled with variable n + 1 is created and made a right sibling of v.

add_var_before

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

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.

add_var_before_lca

Let v be the smallest vtree which contains the variables of literals, where count is the number of literals. A new leaf node labeled with variable n + 1 is created and made a left sibling of v.

apply

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

auto_gc_and_minimize_off

Deactivates automatic garbage collection and automatic SDD minimization.

auto_gc_and_minimize_on

Activates automatic garbage collection and automatic SDD minimization.

condition

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

conjoin

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

copy

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

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

dead_count

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

dead_size

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

disjoin

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

dot

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

dot_shared

Shared SDD, formatted for use with Graphviz dot.

exists

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

exists_multiple

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

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

Returns an SDD representing the function false.

fnf_to_sdd
forall

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

from_cnf_file

Create an SDD from the given CNF file.

from_cnf_string

Create an SDD from the given CNF string.

from_dnf_file

Create an SDD from the given DNF file.

from_dnf_string

Create an SDD from the given DNF string.

from_fnf

Create an SDD from the given DNF file.

from_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

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

get_vars
global_minimize_cardinality

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

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

init_vtree_size_limit

Declares the size s of current SDD for vtree as the reference size for the relative size limit l.

That is, a rotation or swap operation will fail if the SDD size grows to larger than s × l.

is_auto_gc_and_minimize_on

Is automatic garbage collection and automatic SDD minimization activated?

is_prevent_transformation_on

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

is_var_used

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

Parameters:var – Literal (number)
l

Short for literal(lit)

lca_of_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

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

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

live_size

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

minimize

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

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

minimize_limited
minimum_cardinality

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

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

move_var_after

Let v be the vtree leaf node labeled with variable target var. The leaf node labeled with variable var is moved to become a right sibling of leaf v.

move_var_after_last

Let v be the rightmost leaf node in the vtree. The leaf node labeled with variable var is moved to become a right sibling of leaf v.

move_var_before

Let v be the vtree leaf node labeled with variable target var. The leaf node labeled with variable var is moved to become a left sibling of leaf v.

move_var_before_first

Let v be the leftmost leaf node in the vtree. The leaf node labeled with variable var is moved to become a left sibling of leaf v.

negate

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

print_stdout
read_cnf_file

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

read_dnf_file

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

read_sdd_file

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.

remove_var_added_last

Let v be the vtree leaf node with the variable that was added last to the vtree. This leaf is removed from the vtree.

rename_variables

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

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

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

set_options
set_prevent_transformation

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

set_vtree_apply_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

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

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

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

set_vtree_operation_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

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

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

size

Returns the size of all SDD nodes in the manager.

true

Returns an SDD representing the function true.

update_vtree_size_limit

Updates the reference size for relative size limits.

It is preferrable to invoke this function, as it is more efficent than the function sdd manager init vtree size limit as it does not directly recompute the size of vtree.

var_count

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

var_order

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
vtree_copy
vtree_minimize

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

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